[Haskell-cafe] why GHC cannot infer type in this case?

[Dmitry Kulagin]

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, <oleg at okmij.org> wrote:

>
> 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
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20130203/98970636/attachment.htm>