oleg | 1 Feb 09:09 2013

why GHC cannot infer type in this case?


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

(Continue reading)

Dmitry Kulagin | 3 Feb 19:07 2013
Picon

Re: why GHC cannot infer type in this case?

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



_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane