Dmitry Kulagin wrote:
I try to implement little typed DSL with functions, but there is a problem: compiler is unable to infer type for my "functions".
One way to avoid the problem is to start with the tagless final representation. It imposes fewer requirements on the type system, and is a quite mechanical way of embedding DSL. The enclosed code re-implements your example in the tagless final style. If later you must have a GADT representation, one can easily write an interpreter that interprets your terms as GADTs (this is mechanical). For more examples, see the (relatively recent) lecture notes http://okmij.org/ftp/tagless-final/course/lecture.pdf {-# LANGUAGE TypeOperators, KindSignatures, DataKinds #-} {-# LANGUAGE NoMonomorphismRestriction, TypeFamilies #-} module TestExp where -- types of DSL terms data Ty = Int16 | TFun [Ty] Ty | TSeq [Ty] -- DSL terms class Exp (repr :: Ty -> *) where int16:: Int -> repr Int16 add :: repr Int16 -> repr Int16 -> repr Int16 decl :: (repr (TSeq ts) -> repr t) -> repr (TFun ts t) call :: repr (TFun ts t) -> repr (TSeq ts) -> repr t -- building and deconstructing sequences unit :: repr (TSeq '[]) cons :: repr t -> repr (TSeq ts) -> repr (TSeq (t ': ts)) deco :: (repr t -> repr (TSeq ts) -> repr w) -> repr (TSeq (t ': ts)) -> repr w -- A few convenience functions deun :: repr (TSeq '[]) -> repr w -> repr w deun _ x = x singleton :: Exp repr => (repr t -> repr w) -> repr (TSeq '[t]) -> repr w singleton body = deco (\x _ -> body x) -- sample terms fun = decl $ singleton (\x -> add (int16 2) x) -- Inferred type -- fun :: Exp repr => repr (TFun ((:) Ty 'Int16 ([] Ty)) 'Int16) test = call fun (cons (int16 3) unit) -- Inferred type -- test :: Exp repr => repr 'Int16 fun2 = decl $ deco (\x -> singleton (\y -> add (int16 2) (add x y))) {- inferred fun2 :: Exp repr => repr (TFun ((:) Ty 'Int16 ((:) Ty 'Int16 ([] Ty))) 'Int16) -} test2 = call fun2 (int16 3 `cons` (int16 4 `cons` unit)) -- Simple evaluator -- Interpret the object type Ty as Haskell type * type family TInterp (t :: Ty) :: * type instance TInterp Int16 = Int type instance TInterp (TFun ts t) = TISeq ts -> TInterp t type instance TInterp (TSeq ts) = TISeq ts type family TISeq (t :: [Ty]) :: * type instance TISeq '[] = () type instance TISeq (t1 ': ts) = (TInterp t1, TISeq ts) newtype R t = R{unR:: TInterp t} instance Exp R where int16 = R add (R x) (R y) = R $ x + y decl f = R $ \args -> unR . f . R $ args call (R f) (R args) = R $ f args unit = R () cons (R x) (R y) = R (x,y) deco f (R (x,y)) = f (R x) (R y) testv = unR test -- 5 tes2tv = unR test2 -- 9