Control.Applicative.Normalized.hs

Control.Applicative.Normalized.hs

{-# LANGUAGE RankNTypes, InstanceSigs, KindSignatures, GADTs, ConstraintKinds, ScopedTypeVariables #-}

-- http://neilsculthorpe.com/publications/constrained-monad-problem.pdf

import GHC.Exts

data NAF :: (* -> Constraint) -> (* -> *) -> * -> * where
  Pure :: a -> NAF c t a
  Ap :: c x => NAF c t (x -> a) -> t x -> NAF c t a

instance Functor (NAF c t) where
  fmap :: (a -> b) -> NAF c t a -> NAF c t b
  fmap f naf = pure f <*> naf

instance Applicative (NAF c t) where
  pure :: a -> NAF c t a
  pure = Pure
  (<*>) :: NAF c t (a -> b) -> NAF c t a -> NAF c t b
  Pure g <*> Pure a = Pure (g a)                   -- homomorphism
  n1 <*> Pure a = Pure (\g -> g a) <*> n1          -- interchange
  n1 <*> Ap n2 tx = Ap (Pure (.) <*> n1 <*> n2) tx -- composition

liftNAF :: c a => t a -> NAF c t a
liftNAF ta = Ap (Pure id) ta --identity

foldNAF ::
     forall a c r t.
     (forall x. x -> r x)
  -> (forall y z. c y => r (y -> z) -> t y -> r z)
  -> NAF c t a
  -> r a
foldNAF pur app = foldNAF'
  where
    foldNAF' :: forall b. NAF c t b -> r b
    foldNAF' (Pure b) = pur b
    foldNAF' (Ap n tx) = app (foldNAF' n) tx