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

[Romulus]

Clear and concise answer.

Thank you.

On Thu, Apr 15, 2010 at 21:24, Daniel Fischer <daniel.is.fischer at web.de>wrote:

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


-- 
Romuald THION
Docteur level 1.0 - Great master access control, +3 against half-dead
"la vie, c'est comme un jeu mal foutu dont on ne connait pas les règles et
où il n'y a pas de sauvegardes"
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20100415/5f323877/attachment.html