Re: [Haskell-cafe] Fundeps and overlapping instances
On Tue, Jun 5, 2012 at 2:25 PM, Gábor Lehel illiss...@gmail.com wrote: The encoded version would be: instance (f a b) = FMap f (HJust a) (HJust b) where type f :$: (HJust a) = HJust b and I think this actually demonstrates a *different* limitation, namely that The RHS of an associated type declaration mentions type variable `b' All such variables must be bound on the LHS which means that the standard encoding doesn't work for this case. From a reddit comment[1] by Reiner Pope it turns out you can actually do this: instance (f a b) = FMap f (HJust a) (HJust b) where type f :$: (HJust a) = HJust (f :$: a) A bit more awkward to write, but we're back to TFs not having any expressivity problem in this department. [1] http://www.reddit.com/r/haskell/comments/ut85i/a_few_typefamilies_nuggets/c4ygefh ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
On Tue, Jun 5, 2012 at 4:18 AM, Etienne Laurin etie...@atnnn.com wrote: Thanks for the idea. Here it is. http://hackage.haskell.org/trac/ghc/wiki/TFvsFD I posted my comments on the matter along with many additional comments and examples that I found. Thanks! One part is confusing me. In the section on Partial application, you write: Type synonyms can manipulate constraint kinds but can not use them. The following code doesn't make sense. class (f :$: a) ~ b = FMap (f :: * - * - Constraint) a b where type f :$: a instance FMap f (HJust a) b where type f :$: (HJust a) = f a b = b The class definition looks like it's meant to parallel the earlier FDs version of FMap by using the standard encoding of FDs with TFs, but the instance declaration doesn't. Is it meant to be demonstrating something else? The encoded version would be: instance (f a b) = FMap f (HJust a) (HJust b) where type f :$: (HJust a) = HJust b and I think this actually demonstrates a *different* limitation, namely that The RHS of an associated type declaration mentions type variable `b' All such variables must be bound on the LHS which means that the standard encoding doesn't work for this case. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
| My take is that we should abandon Fundeps, and concentrate on | introducing overlaps into type functions in a controlled way (what | I've called 'dis- overlapped overlaps'.) | | Abandoning fundeps would be a sad day for type-level programming. | There are many things other than overlaps that you can do with fundeps | and constraint kinds that you cannot currently do with type families, | such as: | | - Partial application or higher-order programming. | - Short-circuit evaluation, lazy evaluation or type-level case. Etienne, I think it would be a good service to make Haskell wiki page describing the difference between fundeps and type families, and in particular describing things that can be done with the former but not the latter. The standard encoding of fundeps using type families is this: With fundeps class C a b | a - b With type failies class (F a ~ b) = C a b where type F a The merit of a wiki page would be to be a single place to find the discussion, the standard encoding and examples of where the standard encoding fails. Simon ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Simon Peyton-Jones simonpj at microsoft.com writes: | My take is that we should abandon Fundeps, and concentrate on | introducing overlaps into type functions in a controlled way (what | I've called 'dis- overlapped overlaps'.) | | Abandoning fundeps would be a sad day for type-level programming. | There are many things other than overlaps that you can do with fundeps | and constraint kinds that you cannot currently do with type families, | such as: | | - Partial application or higher-order programming. | - Short-circuit evaluation, lazy evaluation or type-level case. Etienne, I think it would be a good service to make Haskell wiki page describing the difference between fundeps and type families, and in particular describing things that can be done with the former but not the latter. Simon +1 That would be great. I'll link to Etienne's wiki from the Discussion page I've started for NewAxioms http://hackage.haskell.org/trac/ghc/wiki/NewAxioms In particular, it would be good to tease out where we're getting interference or inter-dependence between different type-level extensions: Overlaps Fundeps UndecidableInstances (that is, breaking the coverage conditions) ScopedTypeVariables Given that that the Fundeps idea is taken from relational theory, and relations is just another way of representing functions, there ought to be close correspondence to type-level functions. To me, NewAxioms is aiming at type-level case, to provide a different style of defining type functions, as well as dis-overlapping overlaps. AntC ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
| Abandoning fundeps would be a sad day for type-level programming. | There are many things other than overlaps that you can do with fundeps | and constraint kinds that you cannot currently do with type families, | such as: | | - Partial application or higher-order programming. | - Short-circuit evaluation, lazy evaluation or type-level case. Etienne, I think it would be a good service to make Haskell wiki page describing the difference between fundeps and type families, and in particular describing things that can be done with the former but not the latter. Simon Thanks for the idea. Here it is. http://hackage.haskell.org/trac/ghc/wiki/TFvsFD I posted my comments on the matter along with many additional comments and examples that I found. +1 That would be great. I'll link to Etienne's wiki from the Discussion page I've started for NewAxioms http://hackage.haskell.org/trac/ghc/wiki/NewAxioms In particular, it would be good to tease out where we're getting interference or inter-dependence between different type-level extensions: Overlaps Fundeps UndecidableInstances (that is, breaking the coverage conditions) ScopedTypeVariables I did not check what extensions were turned on in my examples. Given that that the Fundeps idea is taken from relational theory, and relations is just another way of representing functions, there ought to be close correspondence to type-level functions. I put a few examples of the unexpected behaviour of Fundeps on the Wiki page. To me, NewAxioms is aiming at type-level case, to provide a different style of defining type functions, as well as dis-overlapping overlaps. I am eager to see that in action. Etienne Laurin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Hello, There is no problem if an instances uses a type family in it's assumption---the instances should be accepted only if GHC can see enough of the definition of the type family to ensure that the functional dependency holds. This is exactly the same as what it would do to check that a super class constraint holds. -Iavor On Wed, May 30, 2012 at 11:14 PM, Etienne Laurin etie...@atnnn.com wrote: 2012/5/31 Iavor Diatchki iavor.diatc...@gmail.com: Hello, the notion of a functional dependency is well established, and it was used well before it was introduced to Haskell (for example, take a look at http://en.wikipedia.org/wiki/Functional_dependency). So I'd be weary to redefine it lightly. Indeed, GHC's functional dependencies are not the same. I see you have already talked about this on the GHC bug tracker. http://hackage.haskell.org/trac/ghc/ticket/1241 1. Check that an instance is consistent with itself. For example, this should be rejected: instance C a b because it allows C Int Bool and C Int Char which violate the functional dependency. This check may not always be as straightforward. When would this be a valid instance? instance K a b ⇒ C a b With a few extra extensions, K could be a type family. C currently has the kind (a - b - Constraint), with no mention of functional dependencies. Perhaps the kind of C should include the functional dependencies of C? Etienne Laurin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Hello, 2012/6/1 Iavor Diatchki iavor.diatc...@gmail.com: There is no problem if an instances uses a type family in it's assumption---the instances should be accepted only if GHC can see enough of the definition of the type family to ensure that the functional dependency holds. This is exactly the same as what it would do to check that a super class constraint holds. GHC cannot see enough of the definition because type families are open. The type instances are not guaranteed to all be in scope when the class instance is defined. 2012/6/1 AntC anthony_clay...@clear.net.nz: Some of Oleg's instances are awesome (and almost impenetrable -- the TTypeable code is a tour de force). It's all so *dys-functional* (IMO). It's like a typed Prolog with a different order of evaluation. My take is that we should abandon Fundeps, and concentrate on introducing overlaps into type functions in a controlled way (what I've called 'dis- overlapped overlaps'.) Abandoning fundeps would be a sad day for type-level programming. There are many things other than overlaps that you can do with fundeps and constraint kinds that you cannot currently do with type families, such as: - Partial application or higher-order programming. - Short-circuit evaluation, lazy evaluation or type-level case. To study the differences, I have been porting parts of the Prelude to both type classes and type families. http://code.atnnn.com/projects/type-prelude/repository/entry/Prelude/Type.hs http://code.atnnn.com/projects/type-prelude/repository/entry/Prelude/Type/Families.hs Etienne Laurin On Wed, May 30, 2012 at 11:14 PM, Etienne Laurin etie...@atnnn.com wrote: 1. Check that an instance is consistent with itself. For example, this should be rejected: instance C a b because it allows C Int Bool and C Int Char which violate the functional dependency. This check may not always be as straightforward. When would this be a valid instance? instance K a b ⇒ C a b With a few extra extensions, K could be a type family. C currently has the kind (a - b - Constraint), with no mention of functional dependencies. Perhaps the kind of C should include the functional dependencies of C? ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
2012/5/31 Iavor Diatchki iavor.diatc...@gmail.com: Hello, the notion of a functional dependency is well established, and it was used well before it was introduced to Haskell (for example, take a look at http://en.wikipedia.org/wiki/Functional_dependency). So I'd be weary to redefine it lightly. Indeed, GHC's functional dependencies are not the same. I see you have already talked about this on the GHC bug tracker. http://hackage.haskell.org/trac/ghc/ticket/1241 1. Check that an instance is consistent with itself. For example, this should be rejected: instance C a b because it allows C Int Bool and C Int Char which violate the functional dependency. This check may not always be as straightforward. When would this be a valid instance? instance K a b ⇒ C a b With a few extra extensions, K could be a type family. C currently has the kind (a - b - Constraint), with no mention of functional dependencies. Perhaps the kind of C should include the functional dependencies of C? Etienne Laurin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Iavor Diatchki iavor.diatchki at gmail.com writes: Hello, the notion of a functional dependency is well established, and it was used well before it was introduced to Haskell (for example, take a look at http://en.wikipedia.org/wiki/Functional_dependency). So I'd be weary to redefine it lightly. Yes functional dependency is well established in relational algebra (set theory actually) -- it's about values in attributes. But there's nothing corresponding to typevars (I suppose you might call those patterns of values); there's nothing like overlaps. Perhaps instances with Fundeps should only use H98-style arguments? Perhaps we should disallow overlaps with Fundeps (as Hugs does pretty-much)? I can only understand tricky Fundeps by mentally translating them into type- level functions (and I was doing that before type families/associated types came along). class C a b| a - b=== type family CF a instance C a b === type instance CF a = b And that type instance is rejected because `b' is not in scope. Currently there are all sorts of tricks in instance declarations with overlaps and Fundeps, to achieve the effect of type-level functions. You do end up with instance arguments being all typevars, because the instance selection logic is really going on inside the constraints, with type-level 'helper functions'. Some of Oleg's instances are awesome (and almost impenetrable -- the TTypeable code is a tour de force). It's all so *dys-functional* (IMO). My take is that we should abandon Fundeps, and concentrate on introducing overlaps into type functions in a controlled way (what I've called 'dis- overlapped overlaps'.) AntC ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Hello,
On Wed, Jul 7, 2010 at 2:14 PM, Simon Peyton-Jones simo...@microsoft.comwrote:
We can’t permit overlap for type families because it is *unsound *to do
so (ie you can break “well typed programs don’t go wrong”). But if it’s
unsound for type families, it would not be surprising if it was unsound for
fundeps too. (I don’t think anyone has done a soundness proof for fundeps
+ local constraints + overlapping instances, have they?) And indeed I
think it is.
It would be unsound only if the functional dependencies are not checked
properly (which, as you say, is similar to the check for type families).
Here is an example of a sound overlap:
class C a b | a - b
instance C String Char
instance C [a] a
Indeed, it would be OK to allow this sort of overlap for type families too,
although there it would not be useful, because the more general case
already provides the same information as the more specific one. In the
case of overlapping instances, the more specific instance might provide a
different implementation for the class methods, as usual. (disclaimer:
I'm not a fan of overlapping instancesI think that some of
the alternative proposals, such as the instance chains work, are nicer, but
one would have to do same sort of checks there too).
**
Imagine a system “FDL” that has functional dependencies and local type
constraints. The big deal about this is that you get to exploit type
equalities in **given** constraints. Consider Oleg’s example, cut down a
bit:
** **
class C a b | a - b
instance C Int Bool
newtype N2 a = N2 (forall b. C a b = b)
** **
t2 :: N2 Int
t2 = N2 True
** **
We end up type-checking (True :: forall b. C Int b = b). From the
functional dependency we know that (b~Bool), so the function should
typecheck. GHC rejects this program; FDL would not.
** **
But making use of these extra equalities in “given” constraints is quite
tricky. To see why look first at Example 1:
** **
*module* X where
class C a b | a - b
** **
data T a where
MkT :: C a b = b - T a
** **
** **
*module* M1 where
import X
instance C Int Char where ...
f :: Char - T Int
f c = MkT c
** **
*module* M2 where
import X
instance C Int Bool
g :: T Int - Bool
g (MkT x) = x
** **
*module* Bad where
import M1
import M2
bad :: Char - Bool
bad = g . f
** **
This program is unsound: it lets you cast an Int to a Bool; result is a
seg-fault.
You may say that the problem is the inconsistent functional dependencies
in M1 and M2. But GHC won’t spot that. For type families, to avoid this
we “*eagerly*” check for conflicts in type-family instances. In this
case the conflict would be reported when compiling module Bad, because that
is the first time when both instances are visible together.
**
So any FDL system should also make this eager check for conflicts.
I completely agree with this---we should never allow inconsistent instances
to exist in the same scope.
** **
What about overlap? Here’s Example 2:
** **
{-# LANGUAGE IncoherentInstances #-}
*module* Bad where
import X
-- Overlapping instances
instance C Int Bool -- Instance 1
instance C a [a] -- Instance 2
** **
f :: Char - T Int
f c = MkT c -- Uses Instance 1
** **
g :: T a - a
g (MkT x) = x-- Uses Instance 2
** **
bad :: Char - Int
bad = g . f
**
As in the above example, this program violates the functional dependency on
class C and should be rejected, because the two instances are not
consistent with each other.
But at the moment GHC makes an exception for **existentials**. Consider
Example 3:
** **
class C a b | a - b
** **
-- Overlapping instances
instance C Int Bool -- Instance 1
instance C a [a] -- Instance 2
** **
data T where
MkT :: C a b = a - b - T
** **
f :: Bool - T
f x = MkT (3::Int) x -- Uses Instance 1
** **
g :: T - T
g (MkT n x) = MkT n (reverse x) -- Uses Instance 2
** **
bad :: Bool - T
bad = g . f
** **
This program is malformed for the same reason as the previous one: the two
instances violate the functional dependency on the class.
** **
But even nuking IncoherentInstances altogether is not enough. Consider
this variant of Example 3, call it Example 4:
*module* M where
class C a b | a - b
** **
instance C a [a] -- Instance 2
** **
data T where
MkT :: C a b = a - b - T
** **
g :: T - T
g (MkT n x) = MkT n (reverse x) -- Uses Instance 2
** **
*module*
Re: [Haskell-cafe] Fundeps and overlapping instances
Hello, I disagree with your example. 1. Check that an instance is consistent with itself. For example, this should be rejected: instance C a b because it allows C Int Bool and C Int Char which violate the functional dependency. Functional dependencies are not used to pick types, they are used to pick instances. class C a b | a → b where k ∷ a f ∷ a → Maybe b The functional dependency allows you to have a method such as k that doesn't use all the arguments of the class. I expect to be able to make a instance that works for any b. instance C Int b where k = 2 f _ = Nothing Etienne Laurin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Hello, the notion of a functional dependency is well established, and it was used well before it was introduced to Haskell (for example, take a look at http://en.wikipedia.org/wiki/Functional_dependency). So I'd be weary to redefine it lightly. Note that placing a functional dependency constraint is just one way to allow class methods that don't mention all class variables. If the instances for the class do not satisfy the functional dependency (as in your example), you can refactor your class hierarchy, instead. For example: class D a where k :: a class D a = C a b where f :: a - b instance D Int where k = 2 instance C Int b where f _ = Nothing I hope this helps, -Iavor On Wed, May 30, 2012 at 1:31 PM, Etienne Laurin etie...@atnnn.com wrote: Hello, I disagree with your example. 1. Check that an instance is consistent with itself. For example, this should be rejected: instance C a b because it allows C Int Bool and C Int Char which violate the functional dependency. Functional dependencies are not used to pick types, they are used to pick instances. class C a b | a → b where k ∷ a f ∷ a → Maybe b The functional dependency allows you to have a method such as k that doesn't use all the arguments of the class. I expect to be able to make a instance that works for any b. instance C Int b where k = 2 f _ = Nothing Etienne Laurin ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Gábor Lehel illissius at gmail.com writes: If you're referring to the NewAxioms work Simon linked to ... [snip] ... It seems vaguely similar to a paper on instance chains[2] I saw once. Thanks Gábor for the reference, but I don't think they're very comparable. The instance chains is in context of fundeps and overlaps (as you'd expect from MPJ, since it was him who first introduced fundeps). I know fundeps are 'theoretically' equivalent to type families. But I think the instance chains paper is a good demonstration of why I find fundeps so awkward to follow at the superficial syntax level for type-level programming: - you have to look first to the end of the instance to find the head; - and assume (hope!) that the 'result' is the rightmost typevar; - then backtrack through the list of constraints; - some are only validation limits on the instance; - some are calculating intermediate results (again with their result at right). Instance chains include: - not only resolving overlaps (yes, that's similar to NewAxioms); - but also choosing instances based on type class membership; (often asked for by newbies, but really difficult to implement) - and explicit failure leading to backtracking search (Explicit failure is missing from NewAxioms. I don't mean backtracking, but at least treating certain conditions as no instance match. Oleg's HList work needs that (for example in the Lacks constraint), but has to fudge it by putting a fake instance with a fake constraint.) Does the overall instance chain structure guarantee termination of type inference? I don't follow the algebra enough to be sure. Morris Jones' examples seem to me contrived: they've set up overlapping instances where you could avoid them, and even where they seem harder to follow. Yes, their solution is simpler than the problem they start with; but no, the problem didn't need to be that complex in the first case. (I'm looking especially at the GCD/Subt/Lte example -- I think I could get that to work in Hugs with fundeps and no overlaps.) I'm surprised there isn't a Monad Transformer example: [3] by MPJ uses overlaps for MonadT. And MonadT was (I thought) what gave all the trouble with overlaps and default instances and silently changing behaviour. (There's a brief example in Morris' supporting survey - ref [11] in [2].) Anybody out there can explain further? AntC [2] http://citeseerx.ist.psu.edu/viewdoc/download? doi=10.1.1.170.9113rep=rep1type=pdf [3] Functional Programming with Overloading and Higher-Order Polymorphism Mark P. Jones, 1995 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Gábor Lehel illissius at gmail.com writes: On Fri, May 25, 2012 at 7:06 AM, AntC anthony_clayden at clear.net.nz wrote: But it looks like the work SPJ pointed to is using closed style. ... If you're referring to the NewAxioms work Simon linked to in the other thread, I don't see it explicitly stated that all instances have to be within a single module. Especially section 3.3 (Translation) of the pdf[1] seems to suggest otherwise. Though it also doesn't seem to be the same as what you're asking for. As far as I can tell, with NewAxioms, wherever you could currently have a type instance, you could instead have a type instance group. ... [snip] Thanks Gábor, I think you could be right. (It needs some pretty close reading of the equations.) I think in this case an example would be worth a thousand typevars - double-barred of course. I told them in Hebrew, I told them in Dutch, I told them in Latin and Greek, But I clear forgot (and it vexes me much), That Haskell is what they speak. The NewAxioms (draft) paper has a reference to Oleg's HList, but not his Type- level Typeable, nor to Salzmann Stuckey (2002), Chameleon, nor the myriad discussions in the cafe and Haskell Prime. It would be nice to see a statement along the lines of: we looked at X, Y and Z, and didn't follow that approach because ...; or we believe that approach can be incorporated like this ... I thought it was a good research discipline to start with a literature survey, to avoid re-inventing the wheel(?) It seems vaguely similar to a paper on instance chains[2] I saw once. Thanks, I saw that a while back but didn't look into it much at the time. There's heaps of approaches out there to type-safe overlaps. Perhaps they're all logically equivalent(?) So perhaps we're only bikeshedding about surface syntax(??) AntC ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
On Fri, May 25, 2012 at 7:06 AM, AntC anthony_clay...@clear.net.nz wrote: But it looks like the work SPJ pointed to is using closed style. If all they're trying to do is support HList and similar, I guess that's good enough. I tried to explain all this the best part of a year ago. (Admittedly my explanation was a bit turgid, re-reading it today. And not that I was saying anything that hadn't been said by others -- it's resurfaced several times.) Funny how GHC-central just barrels ahead and ignores all those ideas, apparently without explaining why. If you're referring to the NewAxioms work Simon linked to in the other thread, I don't see it explicitly stated that all instances have to be within a single module. Especially section 3.3 (Translation) of the pdf[1] seems to suggest otherwise. Though it also doesn't seem to be the same as what you're asking for. As far as I can tell, with NewAxioms, wherever you could currently have a type instance, you could instead have a type instance group. Within a group you could have unrestricted overlap with the first matching instance being selected, while between groups overlap would continue to be forbidden. Relative to explicit disequality guards it seems both more and less powerful: you couldn't have overlap between modules (but could still split instances among modules as long as they *don't* overlap), but overlap within a module would be more powerful (or at least more convenient). It seems vaguely similar to a paper on instance chains[2] I saw once. (Apologies in advance if any of this is inaccurate, I'm just going by what I can see.) [1] https://docs.google.com/open?id=0B1pOVvPp4fVdOTdjZjU0YWYtYTA5Yy00NmFkLTkxMWUtZmI0NmNhZTQwYzVl [2] http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.170.9113rep=rep1type=pdf ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Simon Peyton-Jones simonpj at microsoft.com writes: [from 7 Jul 2010. I've woken up this thread at Oleg's instigation http://www.haskell.org/pipermail/haskell-prime/2011-July/003491.html ] I'm not going to talk about Fundeps. This is about introducing overlapping instances into type families. But I mean dis-overlapped overlaps, with dis- equality guards on the instances: http://www.haskell.org/pipermail/haskell-prime/2012-May/003689.html This is essentially the same proposal as the July 2011 discussion, but a little updated with actual experience of type families in their more mature form. Example type family equations: type instance F Int = Bool type instance F a | a /~ Int = [a] -- explicit dis-equality guard The July 2010 thread shows how prescient SPJ was about introducing overlaps into type families (or FunDeps). The requirements he ends up with are spot-on, and I believe I have anticipated them in the proposal for dis-overlapped overlaps. Imagine a system “FDL” that has functional dependencies and local type constraints. The big deal about this is that you get to exploit type equalities in *given* constraints. Consider Oleg’s example, cut down a bit: class C a b | a - b instance C Int Bool newtype N2 a = N2 (forall b. C a b = b) t2 :: N2 Int t2 = N2 True We end up type-checking (True :: forall b. C Int b = b). From the functional dependency we know that (b~Bool), so the function should typecheck. GHC rejects this program; FDL would not. GHC 7.2.1 still rejects this program, but accepts a version re-written to use type families: type family CF a type instance CF Int = Bool newtype N2 a = N2 (CF a)-- could be = N2 (forall b. b ~ CF a = b) t2 :: N2 Int t2 = N2 True But making use of these extra equalities in “given” constraints is quite tricky. To see why look first at ... [snip] SPJ works through 4 examples, gathering tricky and nasty situations that are unsound. The examples involve overlaps, so can't be rewritten to use type families. (And GHC rejects attempts to encode them with type classes avoiding fundeps + a functional-dependency-like mechanism (but using equalities) for the result type.) So let me cut to SPJ's conclusions, and compare them against dis-overlapped overlaps ... So FDL must · embody eager checking for inconsistent instances, across modules (Type families already implement this, SPJ notes below.) Yes: I expect dis-overlapped overlaps to do this. (Eager checking is Hugs' approach FWIW, and although at first it seems a nuisance, it leads to more 'crisp' development. Contrast GHC compiles inconsistent instances, but then you find you can't reach them, or get obscure failures.) Eager checking also detects and blocks the irksome imported-instances- silently-changing-behaviour behaviour. · never resolve overlap until only a unique instance can possibly match Yes-ish -- instance matching doesn't have to be as strict as that: type inference must gather evidence of the dis-equality(s) in the guards before matching to the type function equation. Because the instances can't overlap, it's safe to apply the instance, as soon as the dis-equality(s) are discharged, and the head matches. · put all overlapping instances in a single module I don't think we need this, providing each instance 'stands alone' with its dis-equality guards. Instead, for each imported module, we validate that its instances, do not overlap, taking the guards into account. [SPJ admits that such a restriction loses part of the point of overlap in the first place.] Type families already implement the first of these. I believe that if we added the second and third, then overlap of type families would be fine. (I may live to eat my words here.) AntC ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
On 24/05/12 14:14, AntC wrote: Simon Peyton-Jonessimonpjat microsoft.com writes: [from 7 Jul 2010. I've woken up this thread at Oleg's instigation http://www.haskell.org/pipermail/haskell-prime/2011-July/003491.html ] I'm not going to talk about Fundeps. This is about introducing overlapping instances into type families. But I mean dis-overlapped overlaps, with dis- equality guards on the instances: http://www.haskell.org/pipermail/haskell-prime/2012-May/003689.html This is essentially the same proposal as the July 2011 discussion, but a little updated with actual experience of type families in their more mature form. Example type family equations: type instance F Int = Bool type instance F a | a /~ Int = [a] -- explicit dis-equality guard Have you considered the alternative notation where multiple guards are allowed, as in normal function definitions? Something like: type instance F a | a ~ Int = Bool | Otherwise = [a] The last 'otherwise' clause is mandatory, matching should never fall through. Perhaps it could be an error if that were to happen, which would allow you to write closed type functions. Note that Otherwise could be declared in the library as type Otherwise = () :: Constraint I think this variant is almost equivalent to your proposal (so maybe it's just bikeshedding). It is also very similar to the IFEQ proposal, and you can desugar one in terms of the other. I also don't know how hard something like this would be to implement. The matching of type instances would be done in the same way as now, only their expanding is changed. The compiler will at this point have to look which guards are satisfied. In this example the first guard is a~Int, and this can not be checked until more is known about a. So, even though we have a known matching instance, it can not yet be expanded. Perhaps the notation instance F a | a /~ Int is better, because then a type family application can be expanded iff there is a matching instance. Twan ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Fundeps and overlapping instances
Twan van Laarhoven twanvl at gmail.com writes: On 24/05/12 14:14, AntC wrote: Simon Peyton-Jonessimonpjat microsoft.com writes: Have you considered the alternative notation where multiple guards are allowed, as in normal function definitions? Something like: type instance F a | a ~ Int = Bool | Otherwise = [a] Hi Twan, there's various style amongst the discussions -- trace the links back from my previous post to Haskell-prime. And see SPJ's surprise (to me) announcement that there's some work in progress, which gives something very like it. But no, I don't like it: it means I can't put different instances in different modules (so far as I can tell). ..., which would allow you to write closed type functions. Please explain (because I haven't seen this stated anywhere): what is the use case for closed type functions? As opposed to explicitly dis-overlapped type functions. I think this variant is almost equivalent to your proposal ... No: closed functions mean you have to declare all your instances in the same place, in the same module. The whole point of the instance mechanism (or so I thought) is that it's expandable. To see why, consider my example with a 2-argument type function. http://www.haskell.org/pipermail/haskell-prime/2012-May/003690.html (I haven't seen enough detail from the closed type func or IFEQ styles to know whether we could be 'open' on the first arg, but closed on the second.) I also don't know how hard something like this would be to implement. ... Indeed! I've proposed implication constraints, see http://www.haskell.org/pipermail/haskell-prime/2012-May/003689.html That's from the Sulzmann and Stuckey 2002 paper, and I think available for type reasoning in such things as Chameleon. Implication Constraints are used for the OutsideIn(X) approach to implement GADT's with local constraints. (But what I've added is a dis-equality test in the antecedent.) The evidence we need to satisfy the dis-equality guards does not have to be a fully-grounded type, it just needs to be enough that the types can't be equal (typically, the outermost constructor). But it looks like the work SPJ pointed to is using closed style. If all they're trying to do is support HList and similar, I guess that's good enough. I tried to explain all this the best part of a year ago. (Admittedly my explanation was a bit turgid, re-reading it today. And not that I was saying anything that hadn't been said by others -- it's resurfaced several times.) Funny how GHC-central just barrels ahead and ignores all those ideas, apparently without explaining why. AntC ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Fundeps and overlapping instances
Oleg points out, and Martin also mentions, that functional dependencies appear
to interact OK with overlapping instances, but type families do not. I this
impression is mistaken, and I'll try to explain why in this message, in the
hope of exposing any flaws in my reasoning.
We can't permit overlap for type families because it is unsound to do so (ie
you can break well typed programs don't go wrong). But if it's unsound for
type families, it would not be surprising if it was unsound for fundeps too.
(I don't think anyone has done a soundness proof for fundeps + local
constraints + overlapping instances, have they?) And indeed I think it is.
So the short summary of this message is: if it works for fundeps it works for
type families, and vice versa. (NB this equivalence is not true about GHC's
current implementation, however. GHC doesn't support the combination of
fundeps and local constraints at all.)
Such an equivalence doesn't argue against fundeps; I'm only suggesting the that
the two really are very closely equivalent. I much prefer type families from
a programming-style point of view, but that's a subjective opinion.
Simon
Imagine a system FDL that has functional dependencies and local type
constraints. The big deal about this is that you get to exploit type
equalities in *given* constraints. Consider Oleg's example, cut down a bit:
class C a b | a - b
instance C Int Bool
newtype N2 a = N2 (forall b. C a b = b)
t2 :: N2 Int
t2 = N2 True
We end up type-checking (True :: forall b. C Int b = b). From the functional
dependency we know that (b~Bool), so the function should typecheck. GHC
rejects this program; FDL would not.
But making use of these extra equalities in given constraints is quite
tricky. To see why look first at Example 1:
module X where
class C a b | a - b
data T a where
MkT :: C a b = b - T a
module M1 where
import X
instance C Int Char where ...
f :: Char - T Int
f c = MkT c
module M2 where
import X
instance C Int Bool
g :: T Int - Bool
g (MkT x) = x
module Bad where
import M1
import M2
bad :: Char - Bool
bad = g . f
This program is unsound: it lets you cast an Int to a Bool; result is a
seg-fault.
You may say that the problem is the inconsistent functional dependencies in M1
and M2. But GHC won't spot that. For type families, to avoid this we
eagerly check for conflicts in type-family instances. In this case the
conflict would be reported when compiling module Bad, because that is the first
time when both instances are visible together.
So any FDL system should also make this eager check for conflicts.
What about overlap? Here's Example 2:
{-# LANGUAGE IncoherentInstances #-}
module Bad where
import X
-- Overlapping instances
instance C Int Bool -- Instance 1
instance C a [a] -- Instance 2
f :: Char - T Int
f c = MkT c -- Uses Instance 1
g :: T a - a
g (MkT x) = x-- Uses Instance 2
bad :: Char - Int
bad = g . f
Again, a seg fault if it typechecks. But will it? When typechecking 'g', we
get a constraint (C a ?), where 'a' is a skolem constant. Without
IncoherentInstances GHC would reject the program on the grounds that it does
not know what instance to choose. But *with* IncoherentInstances it would
probably go through, which is unsound. So IncoherentInstances has moved from
causing varying dynamic behaviour to causing seg faults.
Very well, so FDL must get rid of IncoherentInstances altogether, at least for
classes that have functional dependencies (or that have superclasses that do).
But at the moment GHC makes an exception for *existentials*. Consider Example
3:
class C a b | a - b
-- Overlapping instances
instance C Int Bool -- Instance 1
instance C a [a] -- Instance 2
data T where
MkT :: C a b = a - b - T
f :: Bool - T
f x = MkT (3::Int) x -- Uses Instance 1
g :: T - T
g (MkT n x) = MkT n (reverse x) -- Uses Instance 2
bad :: Bool - T
bad = g . f
In the pattern match for MkT in g we have the constraint (C a b), where 'a' is
existentially bound. So under GHC's current rules it'll choose the (C a [a])
instance, and conclude that (b ~ [a]). So it's ok to reverse x. But it isn't;
see function bad!
So to avoid unsoundness we must not choose a particular instance from an
overlapping set unless we know, absolutely positively, that the other cases
cannot match.
(GHC's exception for existentials was introduced in response to user demand.
Usually, overlapping instances are somehow semantically coherent, and with an
existential we are *never* going to learn more about the instantiating type, so
choosing the best available seems like a good thing to do.)
But even nuking IncoherentInstances altogether is not enough. Consider this
variant of Example 3, call it Example 4:
module M where
class C a b | a - b
instance C a
