[Haskell-cafe] Quantification in Instance Contexts

[Julian Arni]

Alas, no. I tried to simplify the use case, but in fact the structure is a
DAG, and each node may have multiple parents. So neither "a -> b" nor "b ->
a" hold.


On Wed, Jun 25, 2014 at 3:06 PM, adam vogt <vogt.adam at gmail.com> wrote:

> Hi Julian,
>
> Does each child have only one parent? In other words, is a larger
> "tree" still accepted if you use:
>
> class Child1 a b bool | a b -> bool, b -> a
>
> instead of your Child.
>
> Regards,
> Adam
>
>
> On Wed, Jun 25, 2014 at 5:46 AM, Julian K. Arni <jkarni at gmail.com> wrote:
> > Hi Cafe,
> >
> > I'm playing around with simple logic-programming at the type level. For
> > instance, encoding trees:
> >
> >>> {-# LANGUAGE MultiParamTypeClasses
> >>> , FunctionalDependencies
> >>> , FlexibleInstances
> >>> , UndecidableInstances
> >>> , FlexibleContexts
> >>> , OverlappingInstances #-}
> >>> {-# OPTIONS_GHC -fcontext-stack=100 #-}
> >>>
> >>>
> >>> --     *A
> >>> --    / \
> >>> --  B*   *C
> >>> --   |
> >>> --  D*
> >>>
> >>>
> >>> data A
> >>> data B
> >>> data C
> >>> data D
> >>> class Child a b bool | a b -> bool
> >>> instance Child A B TrueT
> >>> instance Child B D TrueT
> >>> instance Child B C TrueT
> >>> class Path a b bool | a b -> bool
> >
> > Now the following obviously doesn't work (never mind for now that 'Path'
> needs
> > a recursive definition, and that this is really just 'Grandchild'):
> >
> >>> instance (Child a b TrueT, Child b c TrueT) => Path a c TrueT
> >
> > Because 'b' is ambiguous. Fair enough. But I can't directly use a fundep,
> > because 'b' *is* in fact ambiguous. What I want to tell the compiler is
> that
> > it's really okay, since the RHS side (and any possible 'where'
> expressions)
> > doesn't depend on what is instantiated for 'b'.
> >
> > I know I could switch to a class 'Children a bs bool' and encode all
> children
> > of as a type-level list, and then have a fundep between 'a' and 'bs'.
> That's
> > not a *bad* solution: it does give a good sense of the intention. But
> it's not
> > very extensible; really I'd rather be using something like 'forall'
> > - something, I would guess, along the lines of:
> >
> >>> instance forall a c. (forall b. (Child a b TrueT, Child b c TrueT)) =>
> Path
> >>> a c TrueT
> >
> > That, however, fails with:
> >
> >     Malformed instance head: (forall b.
> >                               (Child a b TrueT, Child b c TrueT))
> >                              -> Path a c TrueT
> >     In the instance declaration for ‘Path a c TrueT’
> >
> >
> > So: is there a way (presumably with 'forall') of telling the compiler
> that the
> > ambiguous type 'b' actually won't "leak through" to the RHS, so stop
> bugging me
> > about ambiguity?
> >
> > Thanks,
> >   Julian
> > _______________________________________________
> > Haskell-Cafe mailing list
> > Haskell-Cafe at haskell.org
> > http://www.haskell.org/mailman/listinfo/haskell-cafe
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20140625/502862a3/attachment.html>