That is great! I worked through the paper and played a lot with your code - I must admit that I like this approach much more. I even added to my DSL user-defined types in a type safe way, that I could not do with original GADT-based design. Thank you! Dmitry On Fri, Feb 1, 2013 at 12:09 PM, wrote:

...

I try to implement little typed DSL with functions, but there is a

Dmitry Kulagin wrote: 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