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

[Dmitry Kulagin]

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