src/ForallSem.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE DataKinds #-}
   3 {-# LANGUAGE DeriveFunctor #-}
   4 {-# LANGUAGE AllowAmbiguousTypes #-}
   5 {-# LANGUAGE NoImplicitPrelude #-}
   6 {-# LANGUAGE NoMonomorphismRestriction #-}
   7 {-# LANGUAGE QuantifiedConstraints #-}
   8 {-# LANGUAGE RankNTypes #-}
   9 {-# LANGUAGE ScopedTypeVariables #-}
  10 {-# LANGUAGE StandaloneDeriving #-}
  11 {-# LANGUAGE TypeFamilies #-}
  12 {-# LANGUAGE UndecidableInstances #-}
  13 {-# LANGUAGE UndecidableSuperClasses #-}
  14 {-# LANGUAGE ImportQualifiedPost #-}
  15 {-# LANGUAGE PatternSynonyms #-}
  16 {-# LANGUAGE StandaloneKindSignatures #-}
  17 {-# LANGUAGE PolyKinds #-}
  18 {-# LANGUAGE DataKinds #-}
  19 {-# LANGUAGE ViewPatterns #-}
  20
  21 module ForallSem where
  22
  23 import Data.Functor (Functor(..), (<$>))
  24 import Data.Functor.Constant (Constant(..))
  25 import Control.Applicative (Applicative(..))
  26 import Control.Monad (Monad(..))
  27 import Data.Kind (Type, Constraint)
  28 import Data.Function (($), (.), id)
  29 import Data.String (String)
  30 import Data.Semigroup (Semigroup(..))
  31 import Data.Maybe (Maybe(..), isJust)
  32 import Text.Read (Read(..), reads)
  33 import Data.Bool (otherwise)
  34 import Text.Show (Show(..))
  35 import Data.Eq (Eq(..))
  36 import Data.Either (Either(..))
  37 import Data.Int (Int)
  38 import Prelude (error)
  39 import Control.Monad.Trans.Except qualified as MT
  40 import Control.Monad.Trans.Reader qualified as MT
  41 import Control.Monad.Trans.State qualified as MT
  42 import Type.Reflection
  43 import Unsafe.Coerce (unsafeCoerce)
  44 import Data.Proxy (Proxy(..))
  45 import Prelude qualified
  46 import GHC.Types
  47
  48 type Semantic = Type -> Type
  49 type Syntax = Semantic -> Constraint
  50 class Syn0 (sem::Semantic) where
  51   syn0 :: sem ()
  52 class Syn1 (sem::Semantic) where
  53   syn1 :: sem ()
  54 class Syn2 (sem::Semantic) where
  55   syn2 :: sem () -> sem () -> sem ()
  56
  57 p0 :: (forall sem. syn sem => Syn0 sem) => ForallSem syn ()
  58 p0 = ForallSem syn0
  59
  60 p1 :: (forall sem. syn sem => Syn1 sem) => ForallSem syn ()
  61 p1 = ForallSem syn1
  62
  63 p3 :: forall syn.
  64       ( forall sem. syn sem => Syn0 sem
  65       , forall sem. syn sem => Syn1 sem
  66       , forall sem. syn sem => Syn2 sem
  67       ) => ForallSem syn ()
  68 p3 = ForallSem $ syn2 (unForallSem @syn p0) (unForallSem @syn p1)
  69
  70
  71
  72
  73
  74
  75
  76 data ForallSem (syn::Syntax) (a::Type)
  77    = ForallSem { unForallSem :: forall sem. syn sem => sem a }
  78
  79 instance ( forall sem. syn sem => Functor sem
  80          ) => Functor (ForallSem syn) where
  81   fmap f (ForallSem sem) = ForallSem (fmap f sem)
  82   a <$ (ForallSem sem) = ForallSem (a <$ sem)
  83 instance ( forall sem. syn sem => Applicative sem
  84          , Functor (ForallSem syn)
  85          ) => Applicative (ForallSem syn) where
  86   pure a = ForallSem (pure a)
  87   liftA2 f (ForallSem a) (ForallSem b) = ForallSem (liftA2 f a b)
  88   (<*>) (ForallSem f) (ForallSem a) = ForallSem ((<*>) f a)
  89   (<*) (ForallSem f) (ForallSem a) = ForallSem ((<*) f a)
  90   (*>) (ForallSem f) (ForallSem a) = ForallSem ((*>) f a)
  91 instance ( forall sem. syn sem => Monad sem
  92          , Applicative (ForallSem syn)
  93          ) => Monad (ForallSem syn) where
  94   (>>=) (ForallSem sa) f = ForallSem (sa >>= \a -> case f a of ForallSem sb -> sb)
  95   return = pure
  96   (>>) = (*>)
  97
  98 -- * Interpreter 'Parser'
  99 data TermVT syn = forall vs a. TermVT
 100   { typeTermVT :: Ty vs a
 101   , unTermVT  :: ForallSem syn a
 102   }
 103
 104 -- instance Eq (TyVT) where
 105 --   TyVT x == TyVT y =
 106 --     let (x', y') = appendVars x y in
 107 --     isJust $ eqTypeKi x' y'
 108
 109 -- * Type family @(++)@
 110 type family (++) xs ys where
 111   '[] ++ ys  = ys
 112   -- xs  ++ '[] = xs
 113   (x ': xs) ++ ys = x ': xs ++ ys
 114 infixr 5 ++
 115
 116 -- * Type 'Len'
 117 data Len (xs::[k]) where
 118   LenZ :: Len '[]
 119   LenS :: Len xs -> Len (x ': xs)
 120
 121 instance Show (Len vs) where
 122   showsPrec _p = showsPrec 10 . intLen
 123
 124 addLen :: Len a -> Len b -> Len (a ++ b)
 125 addLen LenZ     b = b
 126 addLen (LenS a) b = LenS $ addLen a b
 127
 128 shiftLen :: forall t b a.  Len a -> Len (a ++      b) -> Len (a ++ t ': b)
 129 shiftLen LenZ b = LenS b
 130 shiftLen (LenS a) (LenS b) = LenS $ shiftLen @t @b a b
 131
 132 intLen :: Len xs -> Int
 133 intLen = go 0
 134   where
 135   go :: Int -> Len xs -> Int
 136   go i LenZ     = i
 137   go i (LenS l) = go (1 Prelude.+ i) l
 138
 139 -- ** Class 'LenInj'
 140 class LenInj (vs::[k]) where
 141   lenInj :: Len vs
 142 instance LenInj '[] where
 143   lenInj = LenZ
 144 instance LenInj as => LenInj (a ': as) where
 145   lenInj = LenS lenInj
 146
 147 type Name = String
 148 -- Use a CUSK, because it's a polymorphically recursive type,
 149 -- See https://ryanglscott.github.io/2020/01/05/five-benefits-to-using-standalonekindsignatures/
 150 data Ty :: forall aK. [Type] -> aK -> Type where
 151   TyConst :: Len vs -> TypeRep a -> Ty vs a
 152   TyVar :: Name -> Var vs a -> Ty vs a
 153   TyApp :: Ty vs f -> Ty vs a -> Ty vs (f a)
 154 infixl 9 `TyApp`
 155 deriving instance Show (Ty vs a)
 156 instance AllocVars Ty where
 157   allocVarsL len (TyConst l c)  = TyConst (addLen len l) c
 158   allocVarsL len (TyApp f a)    = TyApp (allocVarsL len f) (allocVarsL len a)
 159   allocVarsL len (TyVar n v)    = TyVar n (allocVarsL len v)
 160   --allocVarsL len (TyFam l f as) = TyFam (addLen len l) f $ allocVarsL len `mapTys` as
 161
 162   allocVarsR len (TyConst l c)  = TyConst (addLen l len) c
 163   allocVarsR len (TyApp f a)    = TyApp (allocVarsR len f) (allocVarsR len a)
 164   allocVarsR len (TyVar n v)    = TyVar n (allocVarsR len v)
 165   --allocVarsR len (TyFam l f as) = TyFam (addLen l len) f $ allocVarsR len `mapTys` as
 166
 167 data TyVT = forall vs a. TyVT (Ty vs a)
 168 deriving instance Show TyVT
 169 instance Eq TyVT where
 170   TyVT x == TyVT y = isJust (eqTyKi x' y')
 171     where (x', y') = appendVars x y
 172
 173 -- | /Heterogeneous type equality/:
 174 -- return two proofs when two 'Type's are equals:
 175 -- one for the type and one for the kind.
 176 eqTyKi :: Ty vs (x::xK) -> Ty vs (y::yK) -> Maybe (x:~~:y)
 177 eqTyKi (TyConst _lx x) (TyConst _ly y) = eqTypeRep x y
 178 eqTyKi (TyVar   _nx x) (TyVar   _ny y) = eqVarKi   x y
 179 eqTyKi (TyApp fx ax) (TyApp fy ay)
 180  | Just HRefl <- eqTyKi fx fy
 181  , Just HRefl <- eqTyKi ax ay
 182  = Just HRefl
 183 -- eqTyKi (TyFam _ _lx fx ax) (TyFam _ _ly fy ay)
 184 --  | Just HRefl <- eqTypeRep fx fy
 185 --  , Just HRefl <- eqTypes ax ay
 186 --  = Just HRefl
 187 -- -- NOTE: 'TyFam' is expanded as much as possible.
 188 -- eqTyKi x@TyFam{} y = eqTyKi (expandFam x) y
 189 -- eqTyKi x y@TyFam{} = eqTyKi x (expandFam y)
 190 eqTyKi _x _y = Nothing
 191
 192 -- data Some :: (Type -> Type) -> Type where
 193 --   Some :: TypeRep a -> t a -> Some t
 194 --
 195 -- mapSome :: (forall a. s a -> t a) -> Some s -> Some t
 196 -- mapSome f (Some a t) = Some a (f t)
 197 --
 198 -- type SomeTy = Some (Constant ())
 199
 200 -- pattern SomeTy :: TypeRep a -> SomeTy
 201 -- pattern SomeTy a = Some a (Constant ())
 202 -- {-# COMPLETE SomeTy #-}
 203
 204 -- someType :: TypeRep a -> SomeTy
 205 -- someType a = Some a (Constant ())
 206
 207 --infer :: Vars vs -> TermVT syn -> Maybe (TermVT syn)
 208 --infer ctx te = case te of
 209 --Lit i -> return $ Some TTyInt (embed (CInt i))
 210
 211
 212 data Parser syn = Parser
 213   { unParser ::
 214       --MT.State (TokenTerm a)
 215         (Either ErrMsg (TermVT syn))
 216   }
 217
 218 {-
 219 instance ( forall sem. syn sem => Functor sem
 220          ) => Functor (Parser syn) where
 221   fmap f (Parser esa) = Parser $
 222     case esa of
 223       Left e -> Left e
 224       Right (ForallSem sem) -> Right (ForallSem (f <$> sem))
 225   a <$ Parser esa = Parser $
 226     case esa of
 227       Left e -> Left e
 228       Right (ForallSem sem) -> Right (ForallSem (a <$ sem))
 229 instance ( forall sem. syn sem => Applicative sem
 230          , Applicative (ForallSem syn)
 231          , forall err. syn (Either err)
 232          , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
 233          ) => Applicative (Parser syn) where
 234   pure a = Parser (Right (ForallSem (pure a)))
 235   liftA2 f (Parser a) (Parser b) = Parser (liftA2 (liftA2 f) a b)
 236   (<*>) (Parser f) (Parser a) = Parser (liftA2 (<*>) f a)
 237   (*>) (Parser f) (Parser a) = Parser (liftA2 (*>) f a)
 238   (<*) (Parser f) (Parser a) = Parser (liftA2 (<*) f a)
 239 instance ( forall sem. syn sem => Monad sem
 240          , forall err. syn (Either err)
 241          , syn (Parser syn) -- FIXME: what constraint is still missing to still require that?
 242          ) => Monad (Parser syn) where
 243   (>>=) (Parser efsa) f = Parser (efsa >>= \(ForallSem sa) -> sa >>= unParser . f)
 244 -}
 245
 246 -- * Type 'BinTree'
 247 -- | /Binary Tree/.
 248 data BinTree a
 249  =   BinTree0 a
 250  |   BinTree2 (BinTree a) (BinTree a)
 251  deriving (Eq, Show)
 252
 253 type TermAST = BinTree TokenTerm
 254 data TokenTerm
 255    = TokenTermAtom String
 256    | TokenTermAbst String TyVT TermAST
 257    deriving (Show)
 258
 259 tree0 = add (lit 8) (neg (add (lit 1) (lit 2)))
 260 tree1 = mul (add (lit 8) (neg (add (lit 1) (lit 2)))) (lit 2)
 261 tree2 = lam (\(x::sem Int) -> mul (lit 0) (add (lit 1) (lit 2)))
 262 tree0Print = print tree0
 263 tree1Print = print tree1
 264 tree2Print = print tree2
 265
 266 type ErrMsg = String
 267
 268 safeRead :: Read a => String -> Either ErrMsg a
 269 safeRead s = case reads s of
 270                [(x,"")] -> Right x
 271                _        -> Left $ "Read error: " <> s
 272
 273 instance (forall sem. syn sem => Addable sem) => Addable (ForallSem syn) where
 274   lit n = ForallSem (lit n)
 275   neg (ForallSem a) = ForallSem (neg a)
 276   add (ForallSem a) (ForallSem b) = ForallSem (add a b)
 277 instance (forall sem. syn sem => Mulable sem) => Mulable (ForallSem syn) where
 278   mul (ForallSem a) (ForallSem b) = ForallSem (mul a b)
 279 instance ( forall sem. syn sem => Abstractable sem
 280          --, forall sem. syn sem => Typeable sem -- user instance not accepted
 281          --, forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
 282          ) => Abstractable (ForallSem syn) where
 283   ForallSem a2b .@ ForallSem a = ForallSem (a2b .@ a)
 284   lam f = ForallSem (lam (\a -> let ForallSem b = f (forallSem a) in b))
 285     where
 286     -- Safe here because a :: sem a and b :: sem b share the same 'sem'.
 287     forallSem :: sem a -> ForallSem syn a
 288     forallSem a = ForallSem (unsafeCoerce a)
 289
 290
 291
 292 parseAddable ::
 293  ( forall sem. syn sem => Addable sem
 294  , syn (ForallSem syn)
 295  ) =>
 296  (TermAST -> Parser syn) -> TermAST -> Parser syn
 297 parseAddable _final (BinTree0 (TokenTermAtom s))
 298   | Right (i::Int) <- safeRead s
 299   = Parser $ Right $ TermVT (TyConst LenZ typeRep) $ ForallSem @_ @Int $ lit i
 300 parseAddable final (BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT) = Parser $
 301   case final aT of
 302     Parser aE -> do
 303       TermVT aTy (ForallSem a :: ForallSem syn a) <- aE
 304       case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of
 305         Nothing -> Left "TypeError"
 306         Just HRefl -> do
 307           Right $ TermVT aTy $ neg a
 308 parseAddable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Add")) aT) bT) =
 309   Parser $ do
 310     TermVT aTy (ForallSem a :: ForallSem syn a) <- unParser (final aT)
 311     case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of
 312       Nothing -> Left "TypeError"
 313       Just HRefl -> do
 314         TermVT bTy (ForallSem b :: ForallSem syn b) <- unParser (final bT)
 315         case eqTyKi bTy (TyConst (lenVars bTy) (typeRep @Int)) of
 316           Nothing -> Left "TypeError"
 317           Just HRefl -> do
 318             Right $ TermVT aTy $ ForallSem @_ @Int $ add a b
 319 parseAddable _final e = Parser $ Left $ "Invalid tree: " <> show e
 320
 321 --tree0Parser :: (forall sem. syn sem => Addable sem, syn (ForallSem syn)) => Either ErrMsg (ForallSem syn Int)
 322 --tree0Parser = unParser $ parse tree0Print
 323
 324 class    (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem
 325 instance (Addable sem, Mulable sem, Abstractable sem) => FinalSyntaxes sem
 326
 327 parseMulable ::
 328   ( forall sem. syn sem => Mulable sem
 329   , forall sem. syn sem => Addable sem
 330   , syn (ForallSem syn)
 331   ) =>
 332   (TermAST -> Parser syn) -> TermAST -> Parser syn
 333 parseMulable final (BinTree2 (BinTree2 (BinTree0 (TokenTermAtom "Mul")) aT) bT) =
 334   Parser $ do
 335     case (final aT, final bT) of
 336       (Parser aE, Parser bE) -> do
 337         TermVT aTy (ForallSem a :: ForallSem syn a) <- aE
 338         case eqTyKi aTy (TyConst (lenVars aTy) (typeRep @Int)) of
 339           Nothing -> Left "TypeError"
 340           Just HRefl -> do
 341             TermVT bTy (ForallSem b :: ForallSem syn b) <- bE
 342             case eqTyKi bTy (TyConst (lenVars bTy) (typeRep @Int)) of
 343               Nothing -> Left "TypeError"
 344               Just HRefl -> do
 345                     Right $ TermVT aTy (ForallSem @_ @a $ mul a b)
 346 parseMulable final t = parseAddable final t
 347
 348 parseAbstractable ::
 349   ( forall sem. syn sem => Mulable sem
 350   , forall sem. syn sem => Addable sem
 351   , forall sem. syn sem => Abstractable sem
 352   , syn (ForallSem syn)
 353   ) =>
 354   a ~ Int =>
 355   (TermAST -> Parser syn) -> TermAST -> Parser syn
 356 -- TODO: parse variables
 357 parseAbstractable final (BinTree0 (TokenTermAbst n (TyVT (aTy::Ty vs a)) bT)) =
 358   Parser $
 359     case final bT of
 360       Parser bE -> do
 361             TermVT abTy (abF :: ForallSem syn ab) <- bE
 362             case eqTyKi (TyConst (lenVars aTy) (typeRep @Type)) aTy of
 363               Nothing -> Left "TypeError"
 364               Just HRefl -> do
 365                 case abTy of
 366                   FUN iTy bTy ->
 367                     case eqTyKi (TyConst (lenVars bTy) (typeRep @Type)) bTy of
 368                       Nothing -> Left "TypeError"
 369                       Just HRefl -> do
 370                         -- FIXME: appendVars
 371                         case eqTyKi aTy iTy of
 372                           Nothing -> Left "TypeError"
 373                           Just HRefl -> do
 374                             case abF of
 375                               ForallSem ab ->
 376                                 Right $ TermVT abTy $ ForallSem @_ @ab $
 377                                   -- FIXME: Tyable
 378                                   lam (ab .@)
 379                   _ -> Left "TypeError"
 380 parseAbstractable final t = parseMulable final t
 381
 382 pattern FUN :: forall k (fun :: k) vs. ()
 383             => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
 384                       (arg :: TYPE r1) (res :: TYPE r2).
 385                (k ~ Type, fun ~~ (arg -> res))
 386             => Ty vs arg
 387             -> Ty vs res
 388             -> Ty vs fun
 389 pattern FUN arg res <- (TyConst _len (eqTypeRep (typeRep @(->)) -> Just HRefl) `TyApp` arg) `TyApp` res
 390   where FUN arg res = (TyConst (lenVars arg) (typeRep @(->)) `TyApp` arg) `TyApp` res
 391
 392 -- * Class 'LenVars'
 393 -- | Return the 'Len' of the 'Var' context.
 394 class LenVars a where
 395   lenVars :: a -> Len (VarsOf a)
 396
 397 type instance VarsOf (Ty vs a) = vs
 398 instance LenVars (Ty vs a) where
 399   lenVars (TyConst len _c) = len
 400   lenVars (TyApp f _a)     = lenVars f
 401   lenVars (TyVar _n v)     = lenVars v
 402   -- lenVars (TyFam l _f _as) = l
 403
 404 -- * Type family 'VarsOf'
 405 -- | Return the 'Var' context of something.
 406 type family   VarsOf a :: [Type]
 407 type instance VarsOf (Var vs v) = vs
 408 --type instance VarsOf (UsedVars src vs vs') = vs'
 409
 410
 411
 412 -- * Class 'AllocVars'
 413 -- | Allocate 'Var's in a 'Var' context,
 414 -- either to the left or to the right.
 415 class AllocVars (a::[Type] -> k -> Type) where
 416   allocVarsL :: Len len -> a vs x -> a (len ++ vs) x
 417   allocVarsR :: Len len -> a vs x -> a (vs ++ len) x
 418
 419 appendVars ::
 420  AllocVars a =>
 421  AllocVars b =>
 422  LenVars (a vs_x x) =>
 423  LenVars (b vs_y y) =>
 424  VarsOf (a vs_x x) ~ vs_x =>
 425  VarsOf (b vs_y y) ~ vs_y =>
 426  a vs_x (x::kx) ->
 427  b vs_y (y::ky) ->
 428  ( a (vs_x ++ vs_y) x
 429  , b (vs_x ++ vs_y) y )
 430 appendVars x y =
 431   ( allocVarsR (lenVars y) x
 432   , allocVarsL (lenVars x) y
 433   )
 434
 435
 436
 437 -- Var
 438 data Var (vs::[Type]) (v::vK) :: Type where
 439   VarZ :: TypeRep vk -> Len (Proxy (v::vK) ': vs) -> Var (Proxy (v::vK) ': vs) v
 440   VarS :: Var vs v -> Var (not_v ': vs) v
 441 instance AllocVars Var where
 442   allocVarsL LenZ v       = v
 443   allocVarsL (LenS len) v = VarS (allocVarsL len v)
 444
 445   allocVarsR len (VarZ k l) = VarZ k (addLen l len)
 446   allocVarsR len (VarS v)   = VarS (allocVarsR len v)
 447
 448 data VarV vs = forall v. VarV (Var vs v)
 449 instance LenVars (Var vs v) where
 450   lenVars (VarZ _k l) = l
 451   lenVars (VarS v)    = LenS (lenVars v)
 452
 453 deriving instance Show (Var vs v)
 454
 455 eqVarKi :: Var vs x -> Var vs y -> Maybe ((x::kx) :~~: (y::ky))
 456 eqVarKi VarZ{} VarZ{}     = Just HRefl
 457 eqVarKi (VarS x) (VarS y) = eqVarKi x y
 458 eqVarKi _ _               = Nothing
 459
 460 -- Vars
 461 data Vars (vs::[Type]) :: Type where
 462   -- VarsZ represents an empty context.
 463   VarsZ :: Vars '[]
 464   -- A cons stores a variable name and its type,
 465   -- and then the rest of the context.
 466   VarsS :: String -> TypeRep vK -> Vars vs -> Vars (Proxy (v::vK) ': vs)
 467 type instance VarsOf (Vars vs) = vs
 468 instance LenVars (Vars vs) where
 469   lenVars VarsZ = LenZ
 470   lenVars (VarsS _n _kv vs) = LenS $ lenVars vs
 471
 472
 473 -- Vars
 474 data Env :: [Type] -> Type where
 475   ENil :: Env '[]
 476   ECons :: v -> Env vs -> Env (v ': vs)
 477
 478 -- (!) :: Env vs -> Var vs v -> v
 479 -- (ECons x _) ! VarZ = x
 480 -- (ECons _ e) ! (VarS x) = e ! x
 481 -- ENil ! _ = error "GHC can't tell this is impossible"
 482
 483 lookupVars :: String -> Vars vs -> Maybe (VarV vs)
 484 lookupVars _ VarsZ = Nothing
 485 lookupVars n (VarsS vN vK vs)
 486   | n == vN = Just (VarV (VarZ vK (LenS (lenVars vs))))
 487   | otherwise = (\(VarV v) -> VarV (VarS v)) <$> lookupVars n vs
 488
 489
 490 fix :: (a -> a) -> a
 491 fix f = f (fix f)
 492
 493 parse ::
 494   ( forall sem. syn sem => Addable sem
 495   , forall sem. syn sem => Mulable sem
 496   , forall sem. syn sem => Abstractable sem
 497   , syn (ForallSem syn)
 498   ) =>
 499   TermAST -> Parser syn
 500 parse = fix parseAbstractable
 501
 502 tree0ParsePrint :: TermAST
 503 tree0ParsePrint = case parse @FinalSyntaxes tree0Print of
 504   Parser (Left e) -> error e
 505   Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
 506
 507 tree1ParsePrint :: TermAST
 508 tree1ParsePrint = case parse @FinalSyntaxes tree1Print of
 509   Parser (Left e) -> error e
 510   Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
 511
 512 tree2ParsePrint :: TermAST
 513 tree2ParsePrint = case parse @FinalSyntaxes tree2Print of
 514   Parser (Left e) -> error e
 515   Parser (Right (TermVT _ty (ForallSem sem))) -> print sem
 516
 517 class Addable sem where
 518   lit :: Int -> sem Int
 519   neg :: sem Int -> sem Int
 520   add :: sem Int -> sem Int -> sem Int
 521 class Mulable sem where
 522   mul :: sem Int -> sem Int -> sem Int
 523 class Abstractable sem where
 524   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
 525   lam :: Typeable a => (sem a -> sem b) -> sem (a -> b)
 526   -- | Application, aka. unabstract.
 527   (.@) :: sem (a -> b) -> sem a -> sem b
 528
 529
 530 -- * Interpreter 'Printer'
 531 newtype Printer a = Printer { unPrinter :: TermAST }
 532 print :: Printer a -> TermAST
 533 print = unPrinter
 534 print2 :: String -> Printer a1 -> Printer a2 -> Printer a3
 535 print2 n (Printer aT) (Printer bT) = Printer $ BinTree2 (BinTree2 (BinTree0 (TokenTermAtom n)) aT) bT
 536 instance Addable Printer where
 537   lit n = Printer $ BinTree0 (TokenTermAtom (show n))
 538   neg (Printer aT) = Printer $ BinTree2 (BinTree0 (TokenTermAtom "Neg")) aT
 539   add = print2 "Add"
 540 instance Mulable Printer where
 541   mul = print2 "Mul"
 542 instance Abstractable Printer where
 543   Printer f .@ Printer a = Printer $ BinTree2 f a
 544   lam (f::Printer a -> Printer b) = Printer $
 545                                   -- FIXME: Tyable? instead of Typeable?
 546       BinTree0 (TokenTermAbst "x" (TyVT (TyConst (lenInj @_ @'[]) (typeRep @a)))
 547                                   (unPrinter (f (Printer (BinTree0 (TokenTermAtom "x"))))))