public
Created

Typed concatenative language implemented with type level lists.

  • Download Gist
ConcatLang.hs
Haskell
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
-- 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

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.