Bound Demo

Demo.hs

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE StandaloneDeriving #-}
module Demo where

import Control.Monad (ap, void)
import Data.Foldable (asum)

import Control.Lens
import Bound
import Data.Functor.Classes
import Data.Deriving

data TypeF f a =
    TyFInt
  | TyFArr (f a) (f a)
  | TyFAll (Scope () f a)
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

makePrisms ''TypeF

instance (Eq1 f, Monad f) => Eq1 (TypeF f) where
  liftEq = $(makeLiftEq ''TypeF)

instance (Ord1 f, Monad f) => Ord1 (TypeF f) where
  liftCompare = $(makeLiftCompare ''TypeF)

deriveShow1 ''TypeF

instance Bound TypeF where
  TyFInt >>>= _ = TyFInt
  TyFArr ty1 ty2 >>>= f = TyFArr (ty1 >>= f) (ty2 >>= f)
  TyFAll s >>>= f = TyFAll (s >>>= f)

data TermF f a =
    TmFInt Int
  | TmFAdd (f a) (f a)
  | TmFApp (f a) (f a)
  | TmFAbs (f a) (Scope () f a)
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

makePrisms ''TermF

instance (Eq1 f, Monad f) => Eq1 (TermF f) where
  liftEq = $(makeLiftEq ''TermF)

instance (Ord1 f, Monad f) => Ord1 (TermF f) where
  liftCompare = $(makeLiftCompare ''TermF)

deriveShow1 ''TermF

instance Bound TermF where
  TmFInt i >>>= _ = TmFInt i
  TmFAdd tm1 tm2 >>>= f = TmFAdd (tm1 >>= f) (tm2 >>= f)
  TmFApp tm1 tm2 >>>= f = TmFApp (tm1 >>= f) (tm2 >>= f)
  TmFAbs ty s >>>= f = TmFAbs (ty >>= f) (s >>>= f)

data LangSpine a =
    SpVar a
  | SpTerm (TermF LangSpine a)
  | SpType (TypeF LangSpine a)
  deriving (Functor, Foldable, Traversable)

makePrisms ''LangSpine
deriveEq1 ''LangSpine
deriveOrd1 ''LangSpine
deriveShow1 ''LangSpine

instance Eq a => Eq (LangSpine a) where (==) = eq1
instance Ord a => Ord (LangSpine a) where compare = compare1
instance Show a => Show (LangSpine a) where showsPrec = showsPrec1

instance Applicative LangSpine where
  pure = return
  (<*>) = ap

instance Monad LangSpine where
  return = SpVar

  SpVar x >>= f = f x
  SpTerm tm >>= f = SpTerm (tm >>>= f)
  SpType ty >>= f = SpType (ty >>>= f)

data LangVar a =
    LvTmVar a
  | LvTyVar a
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

makePrisms ''LangVar

newtype Term a = Term (LangSpine (LangVar a))
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

newtype Type a = Type (LangSpine (LangVar a))
  deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

makeWrapped ''Term
makeWrapped ''Type

abstractTy :: (a -> Maybe b) -> Type a -> Scope b LangSpine (LangVar a)
abstractTy f (Type ty) =
  abstract (\x -> preview _LvTyVar x >>= f) ty

abstract1Ty :: Eq a => a -> Type a -> Scope () LangSpine (LangVar a)
abstract1Ty x ty =
  abstractTy (\y -> if x == y then Just () else Nothing) ty

instantiateTy :: (b -> Type a) -> Scope b LangSpine (LangVar a) -> Type a
instantiateTy f =
  Type . instantiate (view _Wrapped . f)

instantiate1Ty :: Type a -> Scope () LangSpine (LangVar a) -> Type a
instantiate1Ty ty =
  instantiateTy (const ty)

_TyVar :: Prism' (Type a) a
_TyVar = _Wrapped . _SpVar . _LvTyVar

_TyInt :: Prism' (Type a) ()
_TyInt = _Wrapped . _SpType . _TyFInt

_TyArr :: Prism' (Type a) (Type a, Type a)
_TyArr = _Wrapped . _SpType . _TyFArr . bimapping _Unwrapped _Unwrapped

_TyAll :: Prism' (Type a) (Scope () LangSpine (LangVar a))
_TyAll = _Wrapped . _SpType . _TyFAll

tyVar :: a -> Type a
tyVar = review _TyVar

tyInt :: Type a
tyInt = review _TyInt ()

tyArr :: Type a -> Type a -> Type a
tyArr ty1 ty2 = review _TyArr (ty1, ty2)

tyAll :: Eq a => a -> Type a -> Type a
tyAll a ty = review _TyAll (abstract1Ty a ty)

abstractTm :: (a -> Maybe b) -> Term a -> Scope b LangSpine (LangVar a)
abstractTm f (Term tm) =
  abstract (\x -> preview _LvTmVar x >>= f) tm

abstract1Tm :: Eq a => a -> Term a -> Scope () LangSpine (LangVar a)
abstract1Tm x tm =
  abstractTm (\y -> if x == y then Just () else Nothing) tm

instantiateTm :: (b -> Term a) -> Scope b LangSpine (LangVar a) -> Term a
instantiateTm f =
  Term . instantiate (view _Wrapped . f)

instantiate1Tm :: Term a -> Scope () LangSpine (LangVar a) -> Term a
instantiate1Tm tm =
  instantiateTm (const tm)

_TmVar :: Prism' (Term a) a
_TmVar = _Wrapped . _SpVar . _LvTmVar

_TmInt :: Prism' (Term a) Int
_TmInt =  _Wrapped . _SpTerm . _TmFInt

_TmAdd :: Prism' (Term a) (Term a, Term a)
_TmAdd = _Wrapped . _SpTerm . _TmFAdd . bimapping _Unwrapped _Unwrapped

_TmApp :: Prism' (Term a) (Term a, Term a)
_TmApp = _Wrapped . _SpTerm . _TmFApp . bimapping _Unwrapped _Unwrapped

_TmAbs :: Prism' (Term a) (Type a, Scope () LangSpine (LangVar a))
_TmAbs = _Wrapped . _SpTerm . _TmFAbs . bimapping _Unwrapped id

tmVar :: a -> Term a
tmVar = review _TmVar

tmInt :: Int -> Term a
tmInt = review _TmInt

tmAdd :: Term a -> Term a -> Term a
tmAdd tm1 tm2 = review _TmAdd (tm1, tm2)

tmApp :: Term a -> Term a -> Term a
tmApp tm1 tm2 = review _TmApp (tm1, tm2)

tmAbs :: Eq a => a -> Type a -> Term a -> Term a
tmAbs a ty tm = review _TmAbs (ty, abstract1Tm a tm)

step :: Term a -> Maybe (Term a)
step tm = asum steps
  where
    steps = [
        do
        (tm1, tm2) <- preview _TmAdd tm
        i1 <- preview _TmInt tm1
        i2 <- preview _TmInt tm2
        pure . review _TmInt $ i1 + i2
      , do
        (tm1, tm2) <- preview _TmAdd tm
        _ <- preview _TmInt tm1
        tm2' <- step tm2
        pure . review _TmAdd $ (tm1, tm2')
      , do
        (tm1, tm2) <- preview _TmAdd tm
        tm1' <- step tm1
        pure . review _TmAdd $ (tm1', tm2)
      , do
        (tmF, tmX) <- preview _TmApp tm
        (_, s) <- preview _TmAbs tmF
        pure $ instantiate1Tm tmX s
      , do
        (tmF, tmX) <- preview _TmApp tm
        tmF' <- step tmF
        pure . review _TmApp $ (tmF', tmX)
      ]

eval :: Term a -> Term a
eval tm =
  case step tm of
    Nothing -> tm
    Just tm' -> eval tm'

demo1 :: Term String
demo1 = tmApp (tmApp (tmAbs "x" tyInt (tmAbs "y" (tyVar "x") (tmAdd (tmVar "x") (tmVar "y")))) (tmInt 1)) (tmInt 2)

demo1' :: Term String
demo1' = eval demo2