Dmitry Kulagin | 31 Jan 15:06 2013
Picon

why GHC cannot infer type in this case?

Hi Cafe,

I try to implement little typed DSL with functions, but there is a problem: compiler is unable to infer type for my "functions". It seems that context is clear, but still GHC complains "Could not deduce...".
It is sad because without type inference the DSL will be very difficult to use. 
Could someone explain me why this happens and how it can be avoided?

I use GHC 7.4.2
I tried to distill the code to show the problem (and full error message below it).

Thank you!
Dmitry

{-# LANGUAGE GADTs, KindSignatures, DataKinds #-}
module TestExp where

-- Sequence of DSL's types to represent type of tuple
data TSeq where
  TSeqEmpty :: TSeq
  TSeqCons :: TypeExp -> TSeq -> TSeq

-- All types allowed in DSL
data TypeExp where
  -- Primitive type
  TInt16 :: TypeExp
  -- Function type is built from types of arguments (TSeq) and type of result
  TFun :: TSeq -> TypeExp -> TypeExp

-- Sequence of expressions to represent tuple
data Seq (t :: TSeq) where
  SeqEmpty :: Seq TSeqEmpty
  SeqCons :: Exp w -> Seq v -> Seq (TSeqCons w v)

data Exp (r :: TypeExp) where
  Decl :: (Seq args -> Exp r) -> Exp (TFun args r)
  Call :: Exp (TFun args r) -> Seq args -> Exp r
  Int16 :: Int -> Exp TInt16
  Add :: Exp TInt16 -> Exp TInt16 -> Exp TInt16

-- Assumed semantics: fun x = x + 2
-- The following line must be uncommented to compile without errors
-- fun :: Exp (TFun (TSeqCons TInt16 TSeqEmpty) TInt16)
fun = Decl $ \(SeqCons x SeqEmpty) -> Add (Int16 2) x


-- eval (Int16 x) = x
-- eval (Call (Decl f) seq) = eval (f seq)
-- eval (Add x y) = eval x + eval y

-- test = eval $ Call fun (SeqCons (Int16 3) SeqEmpty)

----------------- There is full error message: ----------------------------
TestExp.hs:30:53:
    Could not deduce (w ~ 'TInt16)
    from the context (args ~ TSeqCons w v)
      bound by a pattern with constructor
                 SeqCons :: forall (w :: TypeExp) (v :: TSeq).
                            Exp w -> Seq v -> Seq (TSeqCons w v),
               in a lambda abstraction
      at TestExp.hs:30:16-33
    or from (v ~ 'TSeqEmpty)
      bound by a pattern with constructor
                 SeqEmpty :: Seq 'TSeqEmpty,
               in a lambda abstraction
      at TestExp.hs:30:26-33
      `w' is a rigid type variable bound by
          a pattern with constructor
            SeqCons :: forall (w :: TypeExp) (v :: TSeq).
                       Exp w -> Seq v -> Seq (TSeqCons w v),
          in a lambda abstraction
          at TestExp.hs:30:16
    Expected type: Exp 'TInt16
      Actual type: Exp w
    In the second argument of `Add', namely `x'
    In the expression: Add (Int16 2) x


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Andres Löh | 31 Jan 16:27 2013

Re: why GHC cannot infer type in this case?

Hi Dmitry.

> I try to implement little typed DSL with functions, but there is a problem:
> compiler is unable to infer type for my "functions". It seems that context
> is clear, but still GHC complains "Could not deduce...".
> It is sad because without type inference the DSL will be very difficult to
> use.
>
> Could someone explain me why this happens and how it can be avoided?

Pattern matches on GADT generally require type information. Type
inference in such a case is tricky. GADTs are so powerful that in many
cases, there's no unique best type to infer.

As a contrived example, consider this datatype and function:

> data X :: * -> * where
>    C :: Int -> X Int
>    D :: X a
>
> f (C n) = [n]
> f D = []

What should GHC infer for f? Both

> f :: X a -> [Int]
> f :: X a -> [a]

are reasonable choices, but without further information about the
context, it's impossible to say which one of the two is better.

It is theoretically possible to be more clever than GHC is and infer
the types of GADT pattern matches in some cases. However, it is (A) a
lot of work to implement and maintain that cleverness, and (B) it is
then very difficult to describe when exactly a type signature is
required and when it isn't. So GHC adopts the simpler approach and
requires type information for all GADT pattern matches, which is a
simple and predictable rule.

How to prevent such errors in general is difficult to say. In your
particular case, there might be an option, though. If you additionally
use TypeFamilies and FlexibleInstances, you can define:

> class MkDecl d where
>   type MkDeclSeq d :: TSeq
>   type MkDeclRes d :: TypeExp
>   decl' :: d -> Seq (MkDeclSeq d) -> Exp (MkDeclRes d)
>
> instance MkDecl (Exp r) where
>   type MkDeclSeq (Exp r) = TSeqEmpty
>   type MkDeclRes (Exp r) = r
>   decl' e = \ SeqEmpty -> e
>
> instance MkDecl d => MkDecl (Exp w -> d) where
>   type MkDeclSeq (Exp w -> d) = TSeqCons w (MkDeclSeq d)
>   type MkDeclRes (Exp w -> d) = MkDeclRes d
>   decl' f = \ (SeqCons x xs) -> decl' (f x) xs
>
> decl :: MkDecl d => d -> Exp (TFun (MkDeclSeq d) (MkDeclRes d))
> decl d = Decl (decl' d)
>
> fun = decl $ \ x -> Add (Int16 2) x

The idea here is to avoid pattern matching on the GADT, and instead
use an ordinary Haskell function as an argument to the "decl" smart
constructor. We use the type class and two type families to pack that
function (with as many arguments as it has) into the type-level list
and wrap it all up in the original "Decl". This works because on the
outside, no GADT pattern matches are involved, and within the type
class instances, the necessary type information is present.

This is certainly harder to understand than your original version. On
the other hand, it's actually easier to use.

(It's entirely possible that my code can be simplified further. I
haven't thought about this for very long ...)

Cheers,
  Andres

--

-- 
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com
Dmitry Kulagin | 31 Jan 17:52 2013
Picon

Re: why GHC cannot infer type in this case?

Andres, thank you! 

Your response is really helpful. I will try to adopt your suggestion.

Thank again!
Dmitry


On Thu, Jan 31, 2013 at 7:27 PM, Andres Löh <andres <at> well-typed.com> wrote:
Hi Dmitry.

> I try to implement little typed DSL with functions, but there is a problem:
> compiler is unable to infer type for my "functions". It seems that context
> is clear, but still GHC complains "Could not deduce...".
> It is sad because without type inference the DSL will be very difficult to
> use.
>
> Could someone explain me why this happens and how it can be avoided?

Pattern matches on GADT generally require type information. Type
inference in such a case is tricky. GADTs are so powerful that in many
cases, there's no unique best type to infer.

As a contrived example, consider this datatype and function:

> data X :: * -> * where
>    C :: Int -> X Int
>    D :: X a
>
> f (C n) = [n]
> f D = []

What should GHC infer for f? Both

> f :: X a -> [Int]
> f :: X a -> [a]

are reasonable choices, but without further information about the
context, it's impossible to say which one of the two is better.

It is theoretically possible to be more clever than GHC is and infer
the types of GADT pattern matches in some cases. However, it is (A) a
lot of work to implement and maintain that cleverness, and (B) it is
then very difficult to describe when exactly a type signature is
required and when it isn't. So GHC adopts the simpler approach and
requires type information for all GADT pattern matches, which is a
simple and predictable rule.

How to prevent such errors in general is difficult to say. In your
particular case, there might be an option, though. If you additionally
use TypeFamilies and FlexibleInstances, you can define:

> class MkDecl d where
>   type MkDeclSeq d :: TSeq
>   type MkDeclRes d :: TypeExp
>   decl' :: d -> Seq (MkDeclSeq d) -> Exp (MkDeclRes d)
>
> instance MkDecl (Exp r) where
>   type MkDeclSeq (Exp r) = TSeqEmpty
>   type MkDeclRes (Exp r) = r
>   decl' e = \ SeqEmpty -> e
>
> instance MkDecl d => MkDecl (Exp w -> d) where
>   type MkDeclSeq (Exp w -> d) = TSeqCons w (MkDeclSeq d)
>   type MkDeclRes (Exp w -> d) = MkDeclRes d
>   decl' f = \ (SeqCons x xs) -> decl' (f x) xs
>
> decl :: MkDecl d => d -> Exp (TFun (MkDeclSeq d) (MkDeclRes d))
> decl d = Decl (decl' d)
>
> fun = decl $ \ x -> Add (Int16 2) x

The idea here is to avoid pattern matching on the GADT, and instead
use an ordinary Haskell function as an argument to the "decl" smart
constructor. We use the type class and two type families to pack that
function (with as many arguments as it has) into the type-level list
and wrap it all up in the original "Decl". This works because on the
outside, no GADT pattern matches are involved, and within the type
class instances, the necessary type information is present.

This is certainly harder to understand than your original version. On
the other hand, it's actually easier to use.

(It's entirely possible that my code can be simplified further. I
haven't thought about this for very long ...)

Cheers,
  Andres

--
Andres Löh, Haskell Consultant
Well-Typed LLP, http://www.well-typed.com

_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
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

    -- 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
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