[Haskell-cafe] Automating injections: adding a type parameter

[Daniel Fischer]

Am Donnerstag 15 April 2010 19:19:15 schrieb Romulus:
> Hello everyone,
>

>
> I'm stuck with the definition of the helper for LAnd'. I expect :
>
> land' :: ((LAnd' p) :<: (f p)) =>  Mu (f p) ->  Mu (f p) ->  Mu (f p)
> land' = \x y -> inject (LAnd' x y)
>
> ... but ghci 6.10.4 does not really like this definition...
>
>     Could not deduce (LAnd' p :<: f p1)
>       from the context (LAnd' p1 :<: f p1)
>       arising from a use of `inject' at PropSample.hs:128:16-33
>     Possible fix:
>       add (LAnd' p :<: f p1) to the context of
>         the type signature for `land''
>       or add an instance declaration for (LAnd' p :<: f p1)
>     In the expression: inject (LAnd' x y)
>     In the expression: \ x y -> inject (LAnd' x y)
>     In the definition of `land'': land' = \ x y -> inject (LAnd' x y)
> Failed, modules loaded: none.
>
>
>
> Does anybody have a clue for this problem ?
> I don't really understand where is the trouble actually.

The expression (Land' x y) can have the type (Land' q (Mu (f p))) for all 
q. But there's only an instance for the p used in Mu (f p) provided, so

     Could not deduce (LAnd' p :<: f p1)
       from the context (LAnd' p1 :<: f p1)

The solution is to tell the compiler that this expression should have the 
type LAnd' p (Mu (f p)) for the f and p from the type signature, add

{-# LANGUAGE ScopedTypeVariables #-}

and modify land' to

land' :: forall f p. ((LAnd' p) :<: (f p)) =>  Mu (f p) ->  Mu (f p) ->  Mu 
(f p)
land' = \x y -> inject (LAnd' x y :: LAnd' p (Mu (f p)))

to be greeted by


[1 of 1] Compiling Prop             ( PropSample.hs, interpreted )

PropSample.hs:31:16:
    Warning: Declaration of `In' uses deprecated syntax
             Instead, use the form
               In :: {out :: f (Mu f)} -> Mu f
Ok, modules loaded: Prop.
*Prop>

by 6.12.1 and

$ ghci-6.10.3 PropSample
GHCi, version 6.10.3: http://www.haskell.org/ghc/  :? for help
Loading package ghc-prim ... linking ... done.
Loading package integer ... linking ... done.
Loading package base ... linking ... done.
[1 of 1] Compiling Prop             ( PropSample.hs, interpreted )
Ok, modules loaded: Prop.
*Prop>

from the older GHC.

>
> Cheers,
>
> PS: haskellers rulez ;)

+1

>
>
> [1]
> Swierstra, W.
> Data types à la carte
> J. Funct. Program.
> Cambridge University Press, 2008, 18, 423-436
>
> [2]
> Knowles, K.
> First-Order Logic à la Carte
> The Monad.Reader, 2008, issue 11