Typed Lambda the Gathering

> {-# LANGUAGE GADTs #-}
> {-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

> module Typed where

> import Control.Applicative -- (Const(..))
> import Prelude hiding (Left, Right)
> import Data.Functor.Identity
> import qualified Data.Set as Set
> import Data.Set (Set)
> import Unsafe.Coerce

> data Nat

> data Card a where
>     S      :: Card ((a -> b -> c) -> (a -> b) -> a -> c)
>     K      :: Card (a -> b -> a)
>     I      :: Card (a->a)
>     Zero   :: Card Nat
>     Succ   :: Card (Nat -> Nat)
>     Get    :: Card (Nat -> a)
>     Dbl    :: Card (Nat -> Nat)
>     Inc    :: Card (Nat -> (a->a))
>     Dec    :: Card (Nat -> (a->a))
>     Attack :: Card (Nat -> Nat -> Nat -> (a->a))
>     Help   :: Card (Nat -> Nat -> Nat -> (a->a))
>     Copy   :: Card (Nat -> a)
>     Zombie :: Card (Nat -> a -> (a->a))
>     Revive :: Card (Nat -> (a->a))
> deriving instance Show (Card a)
> deriving instance Eq (Card a)

> evalCard :: Card a -> a
> evalCard S = (<*>) -- \f g x -> f x (g x)
> evalCard K = const
> evalCard I = id

Standard Application

> data AppF f a where
>   (:$) :: f (a->b) -> f a -> AppF f b
>   Card :: Card a -> AppF f a

> instance IFunctor AppF where
>     imap f (a :$ b) = f a :$ f b
>     imap _ (Card c) = Card c

> type App = AppF :* Const String

> instance Show (App a) where
>     showsPrec p = getConst . foldFreeI var f where
>       f :: AppF (Const ShowS) :-> Const ShowS
>       f (Card x) = Const $ showsPrec p x
>       f (Const a :$ Const b) = Const $ a . (" (" ++) . b . (')' :)

>       var :: Const String :-> Const ShowS
>       var x = Const $ ('?' :) . (getConst x ++)

> infixl 1 :$

> var :: IFunctor f => String -> (f :* Const String) a
> var = iret . Const

> vars :: App i -> Set String
> vars = getConst . foldFreeI (Const . Set.singleton . getConst) f where
>     f :: AppF (Const (Set String)) :-> Const (Set String)
>     f (Const m :$ Const n) = Const $ Set.union m n
>     f Card{} = Const Set.empty

> eval :: App a -> a
> eval = runIdentity . foldFreeI (error "eval") f where
>   f :: AppF Identity :-> Identity
>   f (a :$ b) = liftA2 ($) a b
>   f (Card c) = Identity $ evalCard c

> coerce :: App i -> App i'
> coerce (Do (m :$ n)) = unsafeCoerce (m |$ n)
> coerce (Do (Card c)) = unsafeCoerce (card c)

> card = Do . Card
> (|$) = (Do.) . (:$)
> s = card S
> k = card K
> i = card I
> zero = card Zero
> succ = card Succ
> s1 a = s |$ a
> s2 a b = s |$ a |$ b
> s3 a b c = s |$ a |$ b |$ c
> k1 a = k |$ a
> k2 a b = k |$ a |$ b
> i1 x = i |$ x

> nat :: Int -> App Nat
> nat 0 = card Zero
> nat 1 = card Succ |$ nat 0
> nat n2 = maybe_s (dbl (nat n)) where
>   n = n2 `div` 2
>   dbl = (card Dbl |$)
>   maybe_s = if n2 `mod` 2 == 0 then id else (card Succ |$)


Sequenced Application

> data SeqApp a where
>     First :: Card a -> SeqApp a
>     Left  :: Card (a->b) -> SeqApp a -> SeqApp b
>     Right :: Card a -> SeqApp (a->b) -> SeqApp b

> deriving instance Show (SeqApp a)

> sk = Left S . Left K
> (|>) = flip ($)

> (~>) :: SeqApp (a->b) -> SeqApp a -> SeqApp b
> exp ~> First x = exp |> Right x
> exp ~> Left x rest = (exp |> sk |> Right x) ~> rest
> exp ~> Right x rest = Right x (sk exp ~> rest)

> right b a = a ~> write b

> write :: App a -> SeqApp a
> write (Do(Card op)) = First op

 Hairy patterns ahead. Could use pattern synonyms to clean up, but she doesn't seem to like ghc 7
 Plus, this definition is not total, it only specifies applications up to arity 4
 A bottom up definition would be total and easier to read, but my brain exploded

 write (Card op :$ x) = Left op $ write x
 write (Card op :$ a :$ b) = write a |> Left op |> right b
 write (Card op :$ a :$ b :$ c) = write a |> Left op |> right b |> right c
 write other = error ("write: not defined for " ++ show other)

> write (Do(Do(Card op) :$ x)) = Left op $ write x
> write (Do(Do(Do(Card op) :$ a) :$ b)) = write a |> Left op |> right b
> write (Do(Do(Do(Do(Card op) :$ a) :$ b) :$ c)) = write a |> Left op |> right b |> right c
> write (Do(Do(Do(Do(Do(Card op) :$ a) :$ b) :$ c) :$ d)) = write a |> Left op |> right b |> right c |> right d

Lambda Calculus

> data ExprF f i where
>   App  :: f (a->b) -> f a -> ExprF f b
>   Lam  :: Const String a -> f b -> ExprF f (a->b)
>   Prim :: Card a -> ExprF f a
>   Lift :: App a -> ExprF f a

> instance IFunctor ExprF where
>     imap f (App m n) = App (f m) (f n)
>     imap f (Lam v m) = Lam v (f m)
>     imap _ (Prim  c) = Prim c
>     imap _ (Lift  e) = Lift e

> type Expr = ExprF :* Const String

> lam = (Do.) . Lam . Const
> app = (Do.) . App
> prim = Do   . Prim  -- Prim is just Card
> lift = Do   . Lift  -- Lift is only necessary elsewhere

> type Env = String -> Int
> testEnv _ = 0

From Lambda Calculus to SKI

> skiContest :: Env -> Expr :-> App
> skiContest env term = foldFreeI pure f term where
>     fv = freeVars term

>     pure :: Const String :-> App
>     pure (Const v)
>       | v `Set.member` fv = card Get |$ nat (env v)
>       | otherwise = var v

>     f :: ExprF App :-> App
>     f (App a b) = a |$ b
>     f (Prim c)  = card c
>     f (Lift x)  = x
>     f (Lam x m) = a x m

>     a :: Const String a -> App b -> App (a->b)
>     a x (Do(m :$ n)) = a x m `s2` a x n

      The second equation is more tricky to type.
      We have no means that two variables with the same label have the same type,

>     a (Const x) (Ret (Const x')) | x == x' = coerce(card I)

>     a x y = k1 y


> skiWiki :: Env -> Expr :-> App
> skiWiki env term = foldFreeI pure f term where
>     fv = freeVars term

>     pure :: Const String :-> App
>     pure (Const v)
>       | v `Set.member` fv = card Get |$ nat (env v)
>       | otherwise = var v

>     f :: ExprF App i -> App i
>     f (App a b) = a |$ b
>     f (Prim c)  = card c
>     f (Lift x)  = x

>     f (Lam (Const v) b) | v `Set.notMember` vars b  = k1 b

>     f (Lam (Const v) (Ret (Const v'))) | v == v' = coerce(card I)
>     f it@(Lam (Const v) (Do(m :$ Ret (Const v'))) :: ExprF App i) | v == v' = coerce m
>     f (Lam v (Do(m :$ n))) = s2 (f $ Lam v m) (f $ Lam v n)


> freeVars :: Expr i -> Set String
> freeVars = getConst . foldFreeI (Const . Set.singleton . getConst) f where
>     f :: ExprF (Const (Set String)) :-> Const (Set String)
>     f (Lam (Const x) (Const b)) = Const $ Set.delete x b
>     f (App (Const m) (Const n)) = Const $ Set.union m n
>     f _ = Const Set.empty


Indexed Free Monads
(Conor McBride, "Kleisli arrows of outrageous fortune")

> type s :-> t = forall i. s i -> t i

> class IFunctor f where imap :: s :-> t -> f s :-> f t

> data (:*) f a i where
>     Ret :: a i -> (f :* a) i
>     Do  :: f (f :* a) i -> (f :* a) i

> instance IFunctor f => IFunctor ((:*) f) where
>     imap f (Ret a) = Ret (f a)
>     imap f (Do fa) = Do $ imap (imap f) fa

> foldFreeI :: IFunctor f => (a :-> b) -> (f b :-> b) -> (f :* a) :-> b
> foldFreeI i _ (Ret x) = i x
> foldFreeI i f (Do it) = f $ imap (foldFreeI i f) it

  we do not really make use of the monadic combinators defined below

> class IMonad m where
>     iret    ::  a :-> m a
>     iextend :: (a :-> m b) -> m a :-> m b

> instance IFunctor f => IMonad ((:*) f) where
>     iret = Ret
>     iextend k (Ret x) = k x
>     iextend k (Do x) = Do $ imap (iextend k) x