Typed concatenative language implemented with type level lists.

ConcatLang.hs

-- Type level implementation of OCaml code from
-- http://alaska-kamtchatka.blogspot.com/2009/01/essence-of-concatenative-languages.html

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}

infixl 4 :->
infixr 5 :-

data TType = TInt | TBol | [TType] :-> [TType]

type family TTypeT (t :: TType) :: *
type instance TTypeT TInt = Int
type instance TTypeT TBol = Bool
type instance TTypeT (r :-> s) = RTypeT r -> RTypeT s

data family RTypeT (r :: [TType]) :: *
data instance RTypeT (t ': r) = TTypeT t :- RTypeT r
data instance RTypeT '[] = E

data Term :: [TType] -> [TType] -> * where
  Id :: Term r r
  I :: Int -> Term r (TInt ': r)
  B :: Bool -> Term r (TBol ': r)
  Q :: Term s t -> Term r ((s :-> t) ': r)
  (:<) :: Term r s -> Term s t -> Term r t
  PAdd :: Term (TInt ': TInt ': r) (TInt ': r)
  PCompose :: Term ((t :-> u) ': (s :-> t) ': r) ((s :-> u) ': r)

eval :: Term r s -> RTypeT r -> RTypeT s
eval Id r = r
eval (I i) r = i :- r
eval (B b) r = b :- r
eval (Q q) r = eval q :- r
eval (a :< b) r = eval b (eval a r)
eval PAdd (i :- j :- r) = i + j :- r
eval PCompose (f :- g :- r) = f . g :- r

run :: Term '[] r -> RTypeT r
run t = eval t E

-- GHC can infer this type:
test :: Term r ((TInt ': s :-> TInt ': s) ': r)
test = Q (I 42) :< Q PAdd :< PCompose

test1 = case run test of 
  f :- E -> case (f (1 :- E)) of 
    x :- E -> x