Re: [Haskell-cafe] Quantification in Instance Contexts

Think about what you're asking from the compiler. If it sees a (Path a c) constraint it would have to magically guess whether there is an intermediate type b for which (Path a b) and (Path b c), which is impossible. Logic programming relies on the closed world assumption, meaning that if a statement cannot be proven within the closed world we are working in then it is false. Haskell typeclasses don't work like this; there is no closed world of types, so the compiler cannot "refute" a constraint. In prolog you'd have something like this: path(A,C) :- path(A,B), path(B,C). (havent used prolog for a while so syntax might be off) If you translate this to first order logic you'd have: \forall A,C.(path(A,C) <- \exists B.(path(A,B)^path(B,C))) It is the existential that is emulated with the cwa and cannot be emulated in haskell's typesystem. On 25 June 2014 07:00, Julian Arni wrote:

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

...

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

...

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

On Wed, Jun 25, 2014 at 5:46 AM, Julian K. Arni wrote: that 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@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe