Re: Is it time to start deprecating FunDeps?
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 wrote:
> > Martin Sulzmann writes:
>
> > > On Wed, May 1, 2013 at 11:13 AM, AntC 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
> Haskell-prime@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime
>
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Is it time to start deprecating FunDeps?
> Martin Sulzmann writes:
> > On Wed, May 1, 2013 at 11:13 AM, AntC 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
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Mobile support
That would be cool! ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Is it time to start deprecating FunDeps?
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 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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Haskell 2014
Dear Haskellers, We are pleased to announce that the Haskell 2014 committee has now formed, and we would be delighted to receive your proposals for changes to the language. Please see http://hackage.haskell.org/trac/haskell-prime/wiki/Process for details on the proposal process. The committee will meet 4 times a year, to consider proposals completed before: * 1st August * 1st November * 1st February * 1st May so if you have been meaning to put the finishing touches to a proposal, then we would encourage you to do so by the end of July! The source for the Haskell report will be updated as proposals are accepted, but new versions of the standard will only be released once a year, during January. The Haskell 2014 committee is comprised of: * Carlos Camarão * Iavor Diatchki * Ian Lynagh (chair) * John Meacham * Neil Mitchell * Ganesh Sittampalam * David Terei * Bas van Dijk * Henk-Jan van Tuyl Thanks Ian (Haskell 2014 committee chair) -- Ian Lynagh, Haskell Consultant Well-Typed LLP, http://www.well-typed.com/ ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Is it time to start deprecating FunDeps?
Comments see below. On Wed, May 1, 2013 at 11:13 AM, AntC wrote: >> 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 > Haskell-prime@haskell.org > http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Is it time to start deprecating FunDeps?
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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Is it time to start deprecating FunDeps?
> 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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Is it time to start deprecating FunDeps?
> AntC writes:
>
> > ...> 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
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: Is it time to start deprecating FunDeps?
(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, 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
> Haskell-prime@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-prime
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
