GADT Lambda Calculator

gadtlambda.hs

{- 
   Andrew Miller 
   
   Authenticated Data Structures, Generically:
     Merkle-ized Lambda Calculator
-}

{-# LANGUAGE GADTs,
  FlexibleInstances, FlexibleContexts, UndecidableInstances,
  StandaloneDeriving, TypeOperators, Rank2Types,
  MultiParamTypeClasses, ConstraintKinds,
  DeriveTraversable, DeriveFunctor, DeriveFoldable,
  TypeFamilies, FunctionalDependencies, 
  ScopedTypeVariables, GeneralizedNewtypeDeriving
 #-}

import Control.Monad
import Control.Monad.Identity
import Prelude hiding (abs)

{- Higher order functors
   from http://www.timphilipwilliams.com/posts/2013-01-16-fixing-gadts.html -}

newtype HFix h a = HFix { unHFix :: h (HFix h) a }
instance (Show (h (HFix h) a)) => Show (HFix h a) where
  show = parens . show . unHFix where
    parens x = "(" ++ x ++ ")"

-- Natural transformation
type f :~> g = forall a. f a -> g a

-- Higher order functor
class HFunctor (h :: (* -> *) -> * -> *) where
    hfmap :: (f :~> g) -> h f :~> h g

-- Higher order catamorphism
hcata :: HFunctor h => (h f :~> f) -> HFix h :~> f
hcata alg = alg . hfmap (hcata alg) . unHFix

-- Standard Functors
newtype I x = I { unI :: x } deriving Show
newtype K x y = K { unK :: x }


-- Something I can't describe
class (HFunctor f, Monad m) => Monadic f d m where
  construct :: forall a. f d a -> m (d a)
  destruct  :: forall a.   d a -> m (f d a)

-- Distributive law requirement here?
-- Laws:
--     forall f. construct <=< destruct . hfmap

instance (HFunctor f) => Monadic f (HFix f) Identity where
  construct = return . HFix
  destruct = return . unHFix




{- CEK Machine interpreter -}

data Term where
data Clo where
data Env where
data Kont where
data Conf where

deriving instance Show Term
deriving instance Show Clo
deriving instance Show Env
deriving instance Show Conf
deriving instance (Show (r a), Show (r Term), Show (r Clo), 
                   Show (r Env), Show (r Kont), Show (r Conf)) => Show (Univ r a)

data Univ :: (* -> *) -> * -> * where
  T   :: r Term -> r Env -> r Kont -> Univ r Conf
  V   :: r Kont -> r Clo           -> Univ r Conf
  CLO :: r Term -> r Env           -> Univ r Clo
  ARG :: r Term -> r Env -> r Kont -> Univ r Kont
  FUN :: r Clo  -> r Kont          -> Univ r Kont
  ENV :: r Clo  -> r Env           -> Univ r Env
--  BASE :: Int -> Univ r Term
  IND :: Int -> Univ r Term
  APP :: r Term -> r Term -> Univ r Term
  ABS :: r Term -> Univ r Term
  STOP  :: Univ r Kont
  ENVE :: Univ r Env
  
instance HFunctor Univ where
  hfmap f (T t e k) = T (f t) (f e) (f k)
  hfmap f (V k v)   = V (f k) (f v)
  hfmap _ ENVE = ENVE
  hfmap _ STOP = STOP


{-
step :: Univ -> Univ
step (T (IND n)     e k)     = V k (e !! n)
step (T (ABS t)     e k)     = V k (CLO t e)
step (T (APP t0 t1) e k)     = T t0 e (Arg t1 e k)
step (T t           e k)     = V k (CLO t e)
step (V (Arg t e k)       v) = T t e (Fun v k)
step (V (Fun (CLO t e) k) v) = T t (v:e) k
-}

instance Monadic Univ (HFix Univ) IO where
  construct = m . HFix   where m x = do { print ("Cnst", x) ; return x }
  destruct  = m . unHFix where m x = do { print ("Dstr", x) ; return x }


nthM :: Monadic Univ d m => Int -> d Env -> m (d Clo)
nthM n = nth n <=< destruct where
  nth 0 (ENV c _) = return c
  nth n (ENV _ e) | n > 0 = nthM (n-1) e
  nth _ _ = error "bad De Bruijn index"

stepM :: Monadic Univ d m => Univ d Conf -> m (Univ d Conf)
stepM (T t' e k) = destruct t' >>= step' where
  step' (IND n) = do { clo <- nthM n e ; return (V k clo) }
  step' (ABS t) = do { clo <- construct (CLO t e) ; return (V k clo) }
  step' (APP t0 t1) = do
    clo <- construct (ARG t1 e k)
    return (T t0 e clo)
--  step' (BASE n) = do { clo <- construct (CLO t' e) ; return (V k clo) }
stepM (V k' v) = destruct k' >>= step' where
  step' (ARG t e k) = do { k' <- construct (FUN v k) ; return (T t e k') }
  step' (FUN c k) = do
    CLO t e <- destruct c
    env <- construct (ENV v e)
    return (T t env k)

injectM :: Monadic Univ d m => d Term -> m (Univ d Conf)
injectM t = do
  enve <- construct ENVE
  stop <- construct STOP
  return (T t enve stop)

evalM :: Monadic Univ d m => d Term -> m (d Clo)
evalM t = injectM t >>= iter where
  iter v@(V s c) = destruct s >>= iter' where
    iter' STOP = return c
    iter' _ = stepM v >>= iter
  iter v = stepM v >>= iter

  
abs = HFix . ABS
app x y = HFix $ APP x y
ind = HFix . IND

fromBool :: Bool -> HFix Univ Term
fromBool False = abs (abs (ind 0))
fromBool True  = abs (abs (ind 1))

tAND   = abs (abs (app (app (ind 1) (ind 0)) (fromBool False)))
tOR    = abs (abs (app (app (ind 1) (fromBool True)) (ind 0)))
tNOT   = abs (abs (abs (app (app (ind 2) (ind 0)) (ind 1))))

fromNat :: Int -> HFix Univ Term
fromNat n = abs (abs (apps n)) where
  apps 0 = ind 0
  apps n = app (ind 1) (apps (n - 1))
  
tSUCC = abs (abs (abs (app (ind 1) (app (app (ind 2) (ind 1)) (ind 0)))))

tY = app (abs (app (ind 0) (ind 0))) (abs (app (ind 0) (ind 0)))

main = do  
  evalM $ app (app tAND (fromBool True)) (fromBool False)
  evalM $ app tNOT (fromBool False)
  evalM $ app tSUCC (fromNat 0)