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