Is it time to start deprecating FunDeps?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
17 messages Options
Reply | Threaded
Open this post in threaded view
|

Is it time to start deprecating FunDeps?

AntC

Now that the Type Equality coercions extension is stable and has been
blessed by SPJ as "a functional-dependency-like mechanism (but using
equalities) for the result type" [in
http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Hig
herranktypesandtypefunctions],
no code is compelled to use FunDeps.

[Note that this is orthogonal to the issue of overlaps. You can use the
equalities mechanism happily with overlaps, see example below.
 This is also orthogonal to type functions/families/associated types. You
can use the equalities mechanism happily without type families.]

There's plenty of code using FunDeps, so we couldn't just withdraw the
extension. But we could start deprecating it.

Better still, given that there is a mechanical way to convert FunDeps to
equalities, we could start treating the FunDep on a class declaration as
documentation, and validate that the instances observe the mechanical
translation.

Here's an example of the mechanical translation for HDeleteMany, the
classic awkward example from HList.

The problem is to delete all occurences of element type e in a HList l.
Here's the 'non-solution' naieve attempt from the HList paper:

    class HDeleteMany e l l' | e l -> l'
    instance HDeleteMany a HNil HNil       -- base case OK
    instance (HList l, HDeleteMany e l l')
          => HDeleteMany e (HCons e l) l'  -- element match, so omit
    instance (HList l, HDeleteMany e l l')
          => HDeleteMany e (HCons e' l) (HCons e' l')
                                           -- element not match, so retain
                                           -- + recurse on the tail

"The two overlapping instance heads for HCons are in no substitution
ordering."

Here's the mechanical translation, which _does_ compile:

    class HDeleteMany e l l'                -- | e l -> l'
    instance (HNil ~ l')                    -- force the result
          => HDeleteMany a HNil l'          -- base case OK
    instance (HList l, HDeleteMany e l l')
          => HDeleteMany e (HCons e l) l'   -- same as above
    instance (HList l, HDeleteMany e l l'', (HCons e' l'') ~ l')
          => HDeleteMany e (HCons e' l) l'  -- force the result

The translation rules (applying for the 'target' term of a FunDep) are:
1. If the target is a bare typevar not appearing otherwise in the head,
   we're done OK.
Otherwise:
2. Replace the target with a fresh typevar.
   (This forces instance match without inspecting the use site.)
3. Add a type equality constraint
   equating the fresh typevar with the as-was target term.
   (This forces the result type, in the same way as a FunDep target.)


Possible GSOC project?




_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

Roman Cheplyaka-2
1. What do you mean by deprecating? Deprecate it in GHC? What does it
   have to do with Haskell'?
2. What do you gain by doing so?
3. How do you translate cyclic dependencies?

Roman

* AntC <[hidden email]> [2013-04-30 05:31:09+0000]

>
> Now that the Type Equality coercions extension is stable and has been
> blessed by SPJ as "a functional-dependency-like mechanism (but using
> equalities) for the result type" [in
> http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Hig
> herranktypesandtypefunctions],
> no code is compelled to use FunDeps.
>
> [Note that this is orthogonal to the issue of overlaps. You can use the
> equalities mechanism happily with overlaps, see example below.
>  This is also orthogonal to type functions/families/associated types. You
> can use the equalities mechanism happily without type families.]
>
> There's plenty of code using FunDeps, so we couldn't just withdraw the
> extension. But we could start deprecating it.
>
> Better still, given that there is a mechanical way to convert FunDeps to
> equalities, we could start treating the FunDep on a class declaration as
> documentation, and validate that the instances observe the mechanical
> translation.
>
> Here's an example of the mechanical translation for HDeleteMany, the
> classic awkward example from HList.
>
> The problem is to delete all occurences of element type e in a HList l.
> Here's the 'non-solution' naieve attempt from the HList paper:
>
>     class HDeleteMany e l l' | e l -> l'
>     instance HDeleteMany a HNil HNil       -- base case OK
>     instance (HList l, HDeleteMany e l l')
>           => HDeleteMany e (HCons e l) l'  -- element match, so omit
>     instance (HList l, HDeleteMany e l l')
>           => HDeleteMany e (HCons e' l) (HCons e' l')
>                                            -- element not match, so retain
>                                            -- + recurse on the tail
>
> "The two overlapping instance heads for HCons are in no substitution
> ordering."
>
> Here's the mechanical translation, which _does_ compile:
>
>     class HDeleteMany e l l'                -- | e l -> l'
>     instance (HNil ~ l')                    -- force the result
>           => HDeleteMany a HNil l'          -- base case OK
>     instance (HList l, HDeleteMany e l l')
>           => HDeleteMany e (HCons e l) l'   -- same as above
>     instance (HList l, HDeleteMany e l l'', (HCons e' l'') ~ l')
>           => HDeleteMany e (HCons e' l) l'  -- force the result
>
> The translation rules (applying for the 'target' term of a FunDep) are:
> 1. If the target is a bare typevar not appearing otherwise in the head,
>    we're done OK.
> Otherwise:
> 2. Replace the target with a fresh typevar.
>    (This forces instance match without inspecting the use site.)
> 3. Add a type equality constraint
>    equating the fresh typevar with the as-was target term.
>    (This forces the result type, in the same way as a FunDep target.)
>
>
> Possible GSOC project?
>
>
>
>
> _______________________________________________
> Haskell-prime mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-prime

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

oleg-30
In reply to this post by AntC

Anthony Clayden wrote:
> Better still, given that there is a mechanical way to convert FunDeps to
> equalities, we could start treating the FunDep on a class declaration as
> documentation, and validate that the instances observe the mechanical
> translation.

I think this mechanical way is not complete. First of all, how do you
mechanically convert something like

        class Sum x y z | x y -> z, x z -> y

Second, in the presence of overlapping, the translation gives
different results: compare the inferred types for t11 and t21. There
is no type improvement in t21.
(The code also exhibits the coherence problem for overlapping instances:
the inferred type of t2 changes when we remove the last instance of
C2, from Bool to [Char].)

{-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances, TypeFamilies #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverlappingInstances #-}

module FD where

class C1 a b | a -> b where
  foo :: a -> b

instance C1 [a] [a] where
    foo = id

instance C1 (Maybe a) (Maybe a) where
    foo = id

{- -- correctly prohibited!
instance x ~ Bool => C1 [Char]  x where
    foo = const True
-}

t1 = foo "a"
t11 = \x -> foo [x]
-- t11 :: t -> [t]

-- Anthony Clayden's translation
class C2 a b where
  foo2 :: a -> b

instance x ~ [a] => C2 [a]  x where
    foo2 = id

instance x ~ (Maybe a) => C2 (Maybe a) x where
    foo2 = id


instance x ~ Bool => C2 [Char]  x where
    foo2 = const True

t2 = foo2 "a"
t21 = \x -> foo2 [x]
-- t21 :: C2 [t] b => t -> b


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

AntC
In reply to this post by Roman Cheplyaka-2
> Roman Cheplyaka <roma@...> writes:
>
> 1. What do you mean by deprecating? Deprecate it in GHC? What does it
>    have to do with Haskell'?
> 2. What do you gain by doing so?

GHC is the de facto testing ground for ideas 'on the menu' for Haskell'.
H' has been in paralysis for years around MPTC, Overlaps, FunDeps/Type
Families (functions). I'm trying to see a way to remove one of the options
so that we can simplify the choices/move the logjam.

So yes, I mean deprecate in GHC.


> 3. How do you translate cyclic dependencies?

You can get an equivalent to cyclic dependencies using equality
constraints. (I'll reply to Oleg's example of Sum.) But I agree that my
mechanical translation doesn't usually get you to the result.

So my GSOC project idea would be to see how far you might get with a more
sophisticated translation.

 
Anthony


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

Andres Löh-3
> You can get an equivalent to cyclic dependencies using equality
> constraints. (I'll reply to Oleg's example of Sum.) But I agree that my
> mechanical translation doesn't usually get you to the result.
>
> So my GSOC project idea would be to see how far you might get with a more
> sophisticated translation.

Just assuming for the moment that you can actually translate fundeps
completely into type equality coercions. Then that would be, to me, a
good reason to (A) make sure that the implementation actually uses
this encoding internally, and (B) keep fundep notation as syntactic
sugar.

I think the main "problem" of the type families vs. fundeps discussion
is that they're two rather involved language extensions that in
addition have very subtle differences. In this situation, you wouldn't
really want to have both be an official part of the language (although
that's the de facto reality we're living in since many years). If,
however, there's a correct and complete unification of the two
concepts in terms of a common underlying formalism, then I don't
necessarily see why we should deprecate one.

Cheers,
  Andres

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

AntC
> Andres Löh <andres.loeh@...> writes:
> ...
>
> I think the main "problem" of the type families vs. fundeps discussion
> is that they're two rather involved language extensions that in
> addition have very subtle differences.

Thanks Andres, but let me be clear: I am _not_ discussing Type Families
vs. FunDeps.

I'm talking about equality constraints only. Yes, equalities and Type
Families arrived (in GHC) at the same time, but they are different
features. (There were many creative ways to achieve something like
equality constraints long before the TF work. For example various
TypeCast's in the HList work. And really the compiler's type inference is
just equality constraint-solving. What arrived in GHC was making
equalities explicit in the surface language, and making sure it integrated
with type inference.)

There are some not-so-subtle differences between TF's and FunDeps.
Especially that FunDeps support overlaps (well, up to a point) -- so no
surprise that the counter-examples in Oleg's post concentrate on overlap
problems.

I am certainly not suggesting that equalities 'solve' those problems. I am
saying they're no worse than FunDeps. And that by taking away FunDeps we
simplify the choices around MPTC's in Haskell Prime.



> ... If, however, there's a correct and complete unification
> of the two concepts in terms of a common underlying formalism,

If by "the two concepts" you mean TF's and FunDeps, then: no, there is no
such unification. (There are many commonalities, but as you say,
subtle/frustrating differences.)

I am claiming FunDeps can be expressed as equality constraints. I'm also
of the opinion that FunDeps require a mental model that doesn't fit well
with a functional language. So I'm arguing for simplification.





_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

AntC
In reply to this post by oleg-30
> <oleg@...> writes:
>
> I think this mechanical way is not complete.

Thanks Oleg for the counter-examples. I find them both rather mischievous,
because they both go beyond the limits of what FunDeps can do:

In your class Sum example,
>
>         class Sum x y z | x y -> z, x z -> y
>
 your own solution has a bunch of helper classes (each with one-
directional FunDeps). Your solution has a single instance declared for the
Sum class, with three bare typevars. So it is valid by step 1. of the
rules I gave. (In your solution all the 'hard work' is done by the
helpers, which are constraints on that single instance.)

(But I do concede that in general the translation rules I gave do not work
for cyclic dependencies. I'm looking into whether I can beef up the rules
to at least validate against a FunDeps class for instances that use EqC's.)


In your overlap example you introduce a definition that won't compile!
>
> {- -- correctly prohibited!
> instance x ~ Bool => C1 [Char]  x where
>     foo = const True
> -}
You expect too much if you think a mechanical translation will 'magic' a
non-compiling program into something that will compile.

I do expect equality constraints to not play well with overlaps. Combining
FunDeps with overlaps is also hazardous. I'm only claiming that EC's will
be at least as good.

In the HDeleteMany example I gave in the OP, yes the translation did solve
a problem that blocked compiling. (And the HList paper also gives a
solution using FunDep's which needs helper classes.) I'm not claiming that
will always work. I'm not claiming that equality constraints are uniformly
better than FunDeps; I'm only claiming that they're at least equivalent in
power, and sometimes give easier to understand code.


And I find FunDeps not very, err, functional.





_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

Edward Kmett-2
In reply to this post by AntC
It seems to be my day to be the villain crying out against everything someone proposes. ;)

I for one would be strongly against a proposal that started actively deprecating the use of functional dependencies in user code. 

There are a number of situations where the sheer amount of code you're forced to write by the mechanical translation to equalities and type families is explosive. I have dozens of classes of forms like

class Wrapped s t a b | a -> s, b -> t, a t -> s, b s -> t

that become frankly nigh unusable after translation -- other examples are much worse. Similarly, in my experience, code written with monads-tf is almost always about 15% more verbose than code written with the mtl. It costs me two characters to put a space and an 's' in for MonadState s m, but I'm usually not talking about the class unless I also reference the state type in the signature later, and there it saves me several characters per occurrence. When you have a more complicated functional dependency set like the above, though the difference isn't just a small constant amount of overhead. 

It isn't that I use these things out of ignorance. I use them deliberately when the alternative isn't palatable.

I'm all for internally desugaring everything into the same form internally, but Haskell as a culture has long embraced surface complexity so long as it can desugar to something internally reasonable: Consider, let vs. where, multiple definitions vs. case, layout vs. {}'s, etc.

This is despite their varying surface complexities. Let is an expression and where being tied to the binding over statements, multiple bindings permitting you to shuffle backtrack pattern matches and guards across several arguments, etc. 

Even changing out the implementation strategy for FDs in GHC has not been without pain, as it has resulted in changing the semantics of a number of corner cases. In fact, one could argue a large part of the stall in there being any progress in standardizing something in the TF vs FD vs both arena has been that it is very much a moving target. The document we would write today bears very little resemblance to the document we'd have written 5 years ago. To standardize something you need to know what it means. If we'd standardized FDs 5 years ago, we'd be sitting here with an increasingly irrelevant language standard today or stuck in our tracks, and with very little practical impact on the community to show for it, and we'd be likely rewriting the whole document now.

It takes a lot of effort to write up something like either TFs or FDs in their full generality, and the resulting document if based on just transcoding the state of GHC documents an implementation, not necessarily the most reasonable commonly agreeable semantics. 

Arguably haskell-prime's role should be to follow far enough behind that the right decisions can be reached by implementations that blaze ahead of it. 

The only Haskell compiler even with type equalities is GHC at this point. They aren't a small change to introduce to a compiler. I for one work on a rather Haskelly compiler for my day job, when I'm not crying gloom and doom on mailing lists, and have been actively considering how to go about it for almost two years now without losing the other properties that make that compiler special. I'd really be a lot more comfortable having seen more success stories of people converting Haskell compilers over to this kind of approach before I felt it wise to say that this way that we know works and which has been productively in use in real code for ten years should be deprecated in favor of a way that only works with the single compiler.

A large part of the pain of "choosing between" FDs and TFs is that both have different somewhat overlapping strengths. In the end I don't think we will wind up choosing between them, we'll just desugar both to a common core. Hopefully after we have more than one point in the design space to choose from.

Removing a language feature just because another one can duplicate it with explosively more verbose code doesn't strike me as a very Haskelly way forward.

-Edward



On Tue, Apr 30, 2013 at 1:31 AM, AntC <[hidden email]> wrote:

Now that the Type Equality coercions extension is stable and has been
blessed by SPJ as "a functional-dependency-like mechanism (but using
equalities) for the result type" [in
http://hackage.haskell.org/trac/ghc/wiki/Records/OverloadedRecordFields#Hig
herranktypesandtypefunctions],
no code is compelled to use FunDeps.

[Note that this is orthogonal to the issue of overlaps. You can use the
equalities mechanism happily with overlaps, see example below.
 This is also orthogonal to type functions/families/associated types. You
can use the equalities mechanism happily without type families.]

There's plenty of code using FunDeps, so we couldn't just withdraw the
extension. But we could start deprecating it.

Better still, given that there is a mechanical way to convert FunDeps to
equalities, we could start treating the FunDep on a class declaration as
documentation, and validate that the instances observe the mechanical
translation.

Here's an example of the mechanical translation for HDeleteMany, the
classic awkward example from HList.

The problem is to delete all occurences of element type e in a HList l.
Here's the 'non-solution' naieve attempt from the HList paper:

    class HDeleteMany e l l' | e l -> l'
    instance HDeleteMany a HNil HNil       -- base case OK
    instance (HList l, HDeleteMany e l l')
          => HDeleteMany e (HCons e l) l'  -- element match, so omit
    instance (HList l, HDeleteMany e l l')
          => HDeleteMany e (HCons e' l) (HCons e' l')
                                           -- element not match, so retain
                                           -- + recurse on the tail

"The two overlapping instance heads for HCons are in no substitution
ordering."

Here's the mechanical translation, which _does_ compile:

    class HDeleteMany e l l'                -- | e l -> l'
    instance (HNil ~ l')                    -- force the result
          => HDeleteMany a HNil l'          -- base case OK
    instance (HList l, HDeleteMany e l l')
          => HDeleteMany e (HCons e l) l'   -- same as above
    instance (HList l, HDeleteMany e l l'', (HCons e' l'') ~ l')
          => HDeleteMany e (HCons e' l) l'  -- force the result

The translation rules (applying for the 'target' term of a FunDep) are:
1. If the target is a bare typevar not appearing otherwise in the head,
   we're done OK.
Otherwise:
2. Replace the target with a fresh typevar.
   (This forces instance match without inspecting the use site.)
3. Add a type equality constraint
   equating the fresh typevar with the as-was target term.
   (This forces the result type, in the same way as a FunDep target.)


Possible GSOC project?




_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

Martin Sulzmann-2
In reply to this post by oleg-30
(1) There's a mechanical way to translate FD programs with
non-overlapping instances to TF (and of course vice versa). For
example, let's reconsider Oleg's example.

> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
> {-# LANGUAGE TypeFamilies #-}
> {-# LANGUAGE FlexibleContexts #-}
>
> class Sum x y z | x y -> z, x z -> y
> instance Sum Int Float Double
>
> class (SumF1 x y ~ z, SumF2 x z ~ y) => SumF x y z
> type family SumF1 x y
> type family SumF2 x z
> instance SumF Int Float Double
> type instance SumF1 Int Float = Double
> type instance SumF2 Int Double = Float

As we know, GHC's intermediate language only records TF type
improvement but not FD type improvement. Therefore,

> f :: SumF Int Float z => z -> z
> f _ = (1.0 :: Double)
>

> {- fails to type check
> f2 :: Sum Int Float z => z -> z
> f2 _ = (1.0 :: Double)
> -}

(2) There's an issue in case of overlapping instances as pointed out by Oleg.
     The source of the issue is that overlapping type class instances
are treated
     differently compared to overlapping type family instances. In principle,
     both formalisms (FD and TF) are equivalent in expressive power.

(3) As Edward points out, there are many good reasons why we want to keep FDs.
     Just compare the above FD program against its TF equivalent!

     I enjoy using both formalisms and would be unhappy if we'd get
rid of one of them :)

-Martin




On Tue, Apr 30, 2013 at 9:18 AM,  <[hidden email]> wrote:

>
> Anthony Clayden wrote:
>> Better still, given that there is a mechanical way to convert FunDeps to
>> equalities, we could start treating the FunDep on a class declaration as
>> documentation, and validate that the instances observe the mechanical
>> translation.
>
> I think this mechanical way is not complete. First of all, how do you
> mechanically convert something like
>
>         class Sum x y z | x y -> z, x z -> y
>
> Second, in the presence of overlapping, the translation gives
> different results: compare the inferred types for t11 and t21. There
> is no type improvement in t21.
> (The code also exhibits the coherence problem for overlapping instances:
> the inferred type of t2 changes when we remove the last instance of
> C2, from Bool to [Char].)
>
> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
> {-# LANGUAGE FlexibleInstances, TypeFamilies #-}
> {-# LANGUAGE NoMonomorphismRestriction #-}
> {-# LANGUAGE OverlappingInstances #-}
>
> module FD where
>
> class C1 a b | a -> b where
>   foo :: a -> b
>
> instance C1 [a] [a] where
>     foo = id
>
> instance C1 (Maybe a) (Maybe a) where
>     foo = id
>
> {- -- correctly prohibited!
> instance x ~ Bool => C1 [Char]  x where
>     foo = const True
> -}
>
> t1 = foo "a"
> t11 = \x -> foo [x]
> -- t11 :: t -> [t]
>
> -- Anthony Clayden's translation
> class C2 a b where
>   foo2 :: a -> b
>
> instance x ~ [a] => C2 [a]  x where
>     foo2 = id
>
> instance x ~ (Maybe a) => C2 (Maybe a) x where
>     foo2 = id
>
>
> instance x ~ Bool => C2 [Char]  x where
>     foo2 = const True
>
> t2 = foo2 "a"
> t21 = \x -> foo2 [x]
> -- t21 :: C2 [t] b => t -> b
>
>
> _______________________________________________
> Haskell-prime mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-prime

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

AntC
In reply to this post by AntC
> AntC <anthony_clayden@...> writes:
>
> > <oleg <at> ...> writes:
> >
> > I think this mechanical way is not complete.
>

On further thought/experiment, I rather think it is -- for one of your
counter examples.

Firstly, I apologise to Oleg. I had mis-remembered his solution to the
class Sum example ...
>
> >
> >         class Sum x y z | x y -> z, x z -> y
> >
>  your own solution has a bunch of helper classes (each with one-
> directional FunDeps).

This Sum is actually a helper called Sum2 in the PeanoArithm module.
Here's Oleg's full code (modulo alpha renaming):
{-
    class Sum2 a b c | a b -> c, a c -> b
    instance Sum2 Z b b
    instance (Sum2 a' b c') => Sum2 (S a') b (S c')

    -- note that in the FunDeps, var a is not a target
    -- so the instances discriminate on var a
-}

And I must apologise to myself for doubting the mechanical translation in
face of cyclical FunDeps. Here it is:

    class Sum2 a b c         -- | a b -> c, a c -> b
    instance (b ~ c) => Sum2 Z b c
    instance (c ~ (S c'), Sum2 a' b c') => Sum2 (S a') b c


> Your [Oleg's] solution has a single instance declared for the
> Sum class, with three bare typevars. So it is valid by step 1. of the
> rules I gave. (In your solution all the 'hard work' is done by the
> helpers, which are constraints on that single instance.)
>

That much I had remembered correctly. So I don't need to change the Sum
class (except to remove the FunDep):

    class Sum a b c          -- | a b -> c, a c -> b, b c -> a
    instance (Sum2 a b c, Sum2 b a c) => Sum a b c

The tests from Oleg's code (ta1, ta2) infer the same types. Test ta3 fails
to compile -- as it does for Oleg.

(My code does need UndecidableInstances, as does Oleg's.)





_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

AntC
In reply to this post by Martin Sulzmann-2
> Martin Sulzmann <martin.sulzmann@...> writes:
>
> (1) There's a mechanical way to translate FD programs with
> non-overlapping instances to TF (and of course vice versa).

Martin, no! no! no! You have completely mis-understood.

I do _not_ _not_ _not_ want to replace FD's with TF's.

I want to replace FD's with Equality Constraints. And that's exactly
because I want to use overlapping.

(You've also failed to understand that the Sum example is for doing Peano
Arith. See the solution I've just posted.)





_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

Ian Lynagh-2
In reply to this post by Edward Kmett-2
On Tue, Apr 30, 2013 at 11:35:10PM -0400, Edward Kmett wrote:
>
> I have dozens of classes of forms like
>
> class Wrapped s t a b | a -> s, b -> t, a t -> s, b s -> t

Isn't this equivalent to just

    class Wrapped s t a b | a -> s, b -> t

?


Thanks
Ian


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

Martin Sulzmann-2
In reply to this post by AntC
Comments see below.

On Wed, May 1, 2013 at 11:13 AM, AntC <[hidden email]> wrote:

>> Martin Sulzmann <martin.sulzmann@...> writes:
>>
>> (1) There's a mechanical way to translate FD programs with
>> non-overlapping instances to TF (and of course vice versa).
>
> Martin, no! no! no! You have completely mis-understood.
>
> I do _not_ _not_ _not_ want to replace FD's with TF's.
>
> I want to replace FD's with Equality Constraints.

Ok, that's the bit I've missed, but then I argue that you can't fully
encode FDs.

Consider again the 'Sum' example.

In the FD world:

Sum x y z1, Sum x y z2  ==> z1 ~ z2

enforced by

Sum x y z | x y -> z

In my TF encoding, we find a similar derivation step

SumF1 x y ~ z1, SumF1 x y ~ z2 ==> z1 ~ z2

So, you're asking can we translate/express FDs using GHC intermediate language
with plain type equations only?

-Martin


> And that's exactly
> because I want to use overlapping.
>
> (You've also failed to understand that the Sum example is for doing Peano
> Arith. See the solution I've just posted.)
>
>
>
>
>
> _______________________________________________
> Haskell-prime mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-prime

_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

Edward Kmett-2
In reply to this post by Ian Lynagh-2
Er, what I meant was

class Foo s t a b | s -> a, t -> b, s b -> t, t a -> s

That is what I get for dashing it off off the cuff. =)

Then s determines some type argument for it, t determines its type argument, but Using s and the other type argument I can determine the whole containing type 't' and vice versa.

instance Foo (Identity a) (Identity b) a b



On Wed, May 1, 2013 at 7:02 AM, Ian Lynagh <[hidden email]> wrote:
On Tue, Apr 30, 2013 at 11:35:10PM -0400, Edward Kmett wrote:
>
> I have dozens of classes of forms like
>
> class Wrapped s t a b | a -> s, b -> t, a t -> s, b s -> t

Isn't this equivalent to just

    class Wrapped s t a b | a -> s, b -> t

?


Thanks
Ian



_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

AntC
In reply to this post by Martin Sulzmann-2
> Martin Sulzmann <martin.sulzmann@...> writes:

> > On Wed, May 1, 2013 at 11:13 AM, AntC <anthony_clayden@...> wrote:
> >
> > I want to replace FD's with Equality Constraints.
>
> Ok, that's the bit I've missed, but then I argue that you can't fully
> encode FDs.
>
> Consider again the 'Sum' example.
>
> In the FD world:
>
> Sum x y z1, Sum x y z2  ==> z1 ~ z2
>
> enforced by
>
> Sum x y z | x y -> z

I'm still not sure you've 'got' it. The class has 2 FD's. Oleg put:
> > >
> > >        class Sum x y z | x y -> z, x z -> y
> > >

>
> In my TF encoding, we find a similar derivation step
>
> SumF1 x y ~ z1, SumF1 x y ~ z2 ==> z1 ~ z2
>

But you haven't captured the FD from {result, arg1} -> arg2.
In the TF example you first posted, you expressed that with an explicit
equality constraint. (I won't repeat yours, because it wasn't to do with
Peano Arith.)


> So, you're asking can we translate/express FDs using GHC intermediate
> language with plain type equations only?

No, not asking, but stating; and not talking about the intermediate
language, but the surface language.

Could I respectfully suggest you re-read the OP.




_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

Edward Kmett-2
Ultimately this is the wrong forum for this discussion as neither type equalities nor functional dependencies are in Haskell' at this time.


On Wed, May 1, 2013 at 7:04 PM, AntC <[hidden email]> wrote:
> Martin Sulzmann <martin.sulzmann@...> writes:

> > On Wed, May 1, 2013 at 11:13 AM, AntC <anthony_clayden@...> wrote:
> >
> > I want to replace FD's with Equality Constraints.
>
> Ok, that's the bit I've missed, but then I argue that you can't fully
> encode FDs.
>
> Consider again the 'Sum' example.
>
> In the FD world:
>
> Sum x y z1, Sum x y z2  ==> z1 ~ z2
>
> enforced by
>
> Sum x y z | x y -> z

I'm still not sure you've 'got' it. The class has 2 FD's. Oleg put:
> > >
> > >        class Sum x y z | x y -> z, x z -> y
> > >

>
> In my TF encoding, we find a similar derivation step
>
> SumF1 x y ~ z1, SumF1 x y ~ z2 ==> z1 ~ z2
>

But you haven't captured the FD from {result, arg1} -> arg2.
In the TF example you first posted, you expressed that with an explicit
equality constraint. (I won't repeat yours, because it wasn't to do with
Peano Arith.)


> So, you're asking can we translate/express FDs using GHC intermediate
> language with plain type equations only?

No, not asking, but stating; and not talking about the intermediate
language, but the surface language.

Could I respectfully suggest you re-read the OP.




_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime


_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime
Reply | Threaded
Open this post in threaded view
|

Re: Is it time to start deprecating FunDeps?

oleg-30
In reply to this post by AntC

> In your class Sum example,
>
>         class Sum x y z | x y -> z, x z -> y
>
> your own solution has a bunch of helper classes

First of all, on the top of other issues, I haven't actually shown an
implementation in the message on Haskell'. I posed this as a general
issue.

In special cases like below

    > class Sum2 a b c | a b -> c, a c -> b
    > instance Sum2 Z b b
    > instance (Sum2 a' b c') => Sum2 (S a') b (S c')

    > -- note that in the FunDeps, var a is not a target
    > -- so the instances discriminate on var a
I didn't doubt the translation would go through because there is a
case analysis on a. But the general case can be more complex. For
example,

class Sum2 a b c | a b -> c, a c -> b
instance Sum2 Z Z Z
instance Sum2 O Z O
instance Sum2 Z O O
instance Sum2 O O Z


> In your overlap example you introduce a definition that won't compile!
> >
> > {- -- correctly prohibited!
> > instance x ~ Bool => C1 [Char]  x where
> >     foo = const True
> > -}
> You expect too much if you think a mechanical translation will 'magic' a
> non-compiling program into something that will compile.

> I do expect equality constraints to not play well with overlaps. Combining
> FunDeps with overlaps is also hazardous. I'm only claiming that EC's will
> be at least as good.

I don't understand the remark. The code marked `correctly prohibited'
is in the comments. There are no claims were made about that code. If
you found that comment disturbing, please delete it. It won't affect the
the example: the types were improved in t11 but were not
improved in t21. Therefore, EC's are not just as good. Functional
dependencies seem to do better.



_______________________________________________
Haskell-prime mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-prime