Re: Fundeps and type equality
Thanks, indeed you're right. For better or worse, so let's extend FC to include FD-style improvement :) Aren't we running then into the same 'type soundness' issues (connected to ordering of overlapping instances) you mention below? There's currently no issue for FDs because FD-style improvement is not manifested in GHC's internal language FC. So, if FD-style improvement will be treated similarly compared to type families, then we might have to rethink the entire case of overlapping type class instances? -Martin On Thu, Jan 10, 2013 at 7:56 PM, Richard Eisenberg e...@cis.upenn.eduwrote: For better or worse, the new overlapping type family instances use a different overlapping mechanism than functional dependencies do. Class instances that overlap are chosen among by order of specificity; overlapping instances can be declared in separate modules. Overlapping family instances must be given an explicit order, and those that overlap must all be in the same module. The decision to make these different was to avoid type soundness issues that would arise with overlapping type family instances declared in separate modules. (Ordering a set of family instance equations by specificity, on the other hand, could easily be done within GHC.) So, as yet, we can't fully encode functional dependencies with type families, I don't think. Richard On Jan 2, 2013, at 4:01 PM, Martin Sulzmann martin.sulzmann.hask...@googlemail.com wrote: I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: Extracting programs from type class proofs (type improvement comes only at the end) Similar to FC, coercions (proof terms) are used to represent type equations (improvement). Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small). It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ... -Martin On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones simo...@microsoft.com wrote: As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). ** ** Iavor is quite right ** ** It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. ** ** Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. ** ** I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions ** ** The main issues are, I think: **· **How to express functional dependencies like “fixing the result type and the first argument will fix the second argument” **· **How to express that idea in the proof language ** ** Simon ** ** *From:* glasgow-haskell-bugs-boun...@haskell.org [mailto: glasgow-haskell-bugs-boun...@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-b...@haskell.org; GHC Users Mailing List *Subject:* Re: Fundeps and type equality ** ** Hello Conal, ** ** GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class). ** ** As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. ** ** In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC. ** ** Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some
Re: Fundeps and type equality
I agree with Iavor that it is fairly straight-forward to extend FC to support FD-style type improvement. In fact, I've formalized such a proof language in a PPDP'06 paper: Extracting programs from type class proofs (type improvement comes only at the end) Similar to FC, coercions (proof terms) are used to represent type equations (improvement). Why extend FC? Why not simply use type families to encode FDs (and thus keep FC simple and small). It's been a while, but as far as I remember, the encoding is only problematic in case of the combination of FDs and overlapping instances. Shouldn't this now be fixable given that type family instances can be overlapping? Maybe I'm missing something, guess it's also time to dig out some old notes ... -Martin On Wed, Jan 2, 2013 at 10:04 AM, Simon Peyton-Jones simo...@microsoft.comwrote: As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). ** ** Iavor is quite right ** ** It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. ** ** Iavor: I don’t think it’s straightforward, but I’m willing to be educated. By all means start a wiki page to explain how, if you think it is. ** ** I do agree that injective type families would be a good thing, and would deal with the main reason that fundeps are sometimes better than type families. A good start would be to begin a wiki page to flesh out the design issues, perhaps linked from http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions ** ** The main issues are, I think: **· **How to express functional dependencies like “fixing the result type and the first argument will fix the second argument” **· **How to express that idea in the proof language ** ** Simon ** ** *From:* glasgow-haskell-bugs-boun...@haskell.org [mailto: glasgow-haskell-bugs-boun...@haskell.org] *On Behalf Of *Iavor Diatchki *Sent:* 26 December 2012 02:48 *To:* Conal Elliott *Cc:* glasgow-haskell-b...@haskell.org; GHC Users Mailing List *Subject:* Re: Fundeps and type equality ** ** Hello Conal, ** ** GHC implementation of functional dependencies is incomplete: it will use functional dependencies during type inference (i.e., to determine the values of free type variables), but it will not use them in proofs, which is what is needed in examples like the one you posted. The reason some proving is needed is that the compiler needs to figure out that for each instantiation of the type `ta` and `tb` will be the same (which, of course, follows directly from the FD on the class). ** ** As far as I understand, the reason that GHC does not construct such proofs is that it can't express them in its internal proof language (System FC). It seems to me that it should be fairly straight-forward to extend FC to support this sort of proof, but I have not been able to convince folks that this is the case. I could elaborate, if there's interest. ** ** In the mean time, the way forward would probably be to express the dependency using type families, which I find tends to be more verbose but, at present, is better supported in GHC. ** ** Cheers, -Iavor PS: cc-ing the GHC users' list, as there was some talk of closing the ghc-bugs list, but I am not sure if the transition happened yet. ** ** ** ** ** ** ** ** On Tue, Dec 25, 2012 at 6:15 PM, Conal Elliott co...@conal.net wrote:*** * I ran into a simple falure with functional dependencies (in GHC 7.4.1): class Foo a ta | a - ta foo :: (Foo a ta, Foo a tb, Eq ta) = ta - tb - Bool foo = (==) I expected that the `a - ta` functional dependency would suffice to prove that `ta ~ tb`, but Pixie/Bug1.hs:9:7: Could not deduce (ta ~ tb) from the context (Foo a ta, Foo a tb, Eq ta) bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) = ta - tb - Bool at Pixie/Bug1.hs:9:1-10 `ta' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) = ta - tb - Bool at Pixie/Bug1.hs:9:1 `tb' is a rigid type variable bound by the type signature for foo :: (Foo a ta, Foo a tb, Eq ta) = ta - tb - Bool at Pixie/Bug1.hs:9:1 Expected type: ta - tb - Bool Actual type: ta - ta - Bool In the expression: (==) In an equation for `foo': foo = (==) Failed, modules loaded: none. Any insights about what's going wrong here? -- Conal ___ Glasgow-haskell-bugs mailing list
Re: Resolving overloading loops for circular constraint graph
2009/9/9 Stefan Holdermans ste...@cs.uu.nl
Dear Martin,
By black-holing you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold.
However, type classes are by default inductive, so there's no
easy fix to offer to your problem.
A propos: are there fundamental objections to coinductive resolving, i.e.,
constructing recursive dictionaries. I suppose termination is hard to
guarantee then: is it enough to require constraints to be productive w.r.t.
instance heads?
Yes, you need instances to be productive, otherwise, you get
bogus cyclic proofs like
instance Foo a = Foo a
dictFooa = dictFooa
You could call this a bug, or simply blame the programmer
for writing down a 'bogus' instance.
Under co-inductive type class solving more (type class) programs will
terminate (my guess). Here are some references:
Satish R. Thatte: Semantics of Type Classes Revisited. LISP and Functional
Programming
1994http://www.informatik.uni-trier.de/%7Eley/db/conf/lfp/lfp1994.html#Thatte94:
208-219
As far as I know, the first paper which talks about co-induction and type
classes.
I myself and some co-workers explored this idea further in some
unpublished draft:
AUTHOR = {M. Sulzmann and J. Wazny and P. J. Stuckey},
TITLE = {Co-induction and Type Improvement in Type Class Proofs},
NOTE = {Manuscript},
YEAR = {2005},
MONTH = {July},
PS = {http://www.cs.mu.oz.au/~sulzmann/manuscript/coind-type-class-proofs.ps
http://www.cs.mu.oz.au/%7Esulzmann/manuscript/coind-type-class-proofs.ps}
I'm quite fond of co-induction because it's such an elegant and powerful
proof technique. However, GHC's co-induction mechanism is fairly limited,
see Simon's reply, so I'm also curious to see what's happening in the
future.
-Martin
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell-cafe] Resolving overloading loops for circular constraint graph
Your example must loop because as you show below
the instance declaration leads to a cycle.
By black-holing you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold.
However, type classes are by default inductive, so there's no
easy fix to offer to your problem.
In any case, this is not a bug, you simply play with fire
once type functions show up in the instance context.
There are sufficient conditions to guarantee termination,
but they are fairly restrictive.
-Martin
2009/9/9 Stefan Holdermans ste...@cs.uu.nl
Manuel, Simon,
I've spotted a hopefully small but for us quite annoying bug in GHC's type
checker: it loops when overloading resolving involves a circular constraint
graph containing type-family applications.
The following program (also attached) demonstrates the problem:
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
type family F a :: *
type instance F Int = (Int, ())
class C a
instance C ()
instance (C (F a), C b) = C (a, b)
f :: C (F a) = a - Int
f _ = 2
main :: IO ()
main = print (f (3 :: Int))
My guess is that the loop is caused by the constraint C (F Int) that arises
from the use of f in main:
C (F Int) = C (Int, ()) = C (F Int)
Indeed, overloading can be resolved successfully by black-holing the
initial constraint, but it seems like the type checker refuses to do so.
Can you confirm my findings?
I'm not sure whether this is a known defect. If it isn't, I'd be more than
happy to issue a report.
Since this problem arises in a piece of very mission-critical code, I would
be pleased to learn about any workarounds.
Thanks in advance,
Stefan
___
Haskell-Cafe mailing list
haskell-c...@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: [Haskell] Re: indirectly recursive dictionaries
On Wed, Mar 18, 2009 at 9:45 AM, Simon Peyton-Jones simo...@microsoft.comwrote: [Redirecting to GHC users.] | Tom Schrijvers wrote: | The cyclic dictionaries approach is a bit fragile. The problem appears to | be here that GHC alternates exhaustive phases of constraint reduction and | functional dependency improvement. The problem is that in your example you | need both for detecting a cycle. The whole thing relies on spotting a loop, and that's inherently a bit fragile. I don't know of any formal work on the subject, although I bet there is some. Satish R. Thatte: Semantics of Type Classes Revisited http://portal.acm.org/citation.cfm?id=182459 The first reference I'm aware of which discusses co-induction in the type class context. There are no recursive dictionaries because Thatte's type class semantics uses run-time type passing (plus method lookup) instead of dictionary-passing. Recursive dictionaries are formalized here Martin Sulzmann: Extracting programs from type class proofs http://portal.acm.org/citation.cfm?id=1140348 There's no work I know of which discusses type inference in the presence of co-inductive type classes (and its subtle consequences as pointed out by Tom's earlier email). Chameleon has supported them using the strategy to apply first improvement before considering co-induction. -Martin GHC's current algorithm does not run functional dependencies sufficiently aggressively, because it treats fundeps a different kind of thing to class constraints. Our new solver, long promised but still in the works, fully integrates type classes with type equalities (fundeps, type functions etc), and so should do a better job here. Roughly speaking, the idea is to combine our ICFP'08 paper [1] with a type-class solver. Since writing the ICFP'08 paper we have found some very useful simplifications; and we also have a new plan for the solving strategy OutsideIn [2]. That said, solving recursive problems is not our primary focus right now -- getting it working is -- so I can't promise that it'll do a better job, but I think it will. | It seems we can convince GHC to do constraint reduction and | improvement in the order we desire. The key is to use the | continuation-passing style -- which forces things to happen in the | right order, both at the run-time and at the compile time. Oleg you are a master at persuading GHC's somewhat ad-hoc implementation to dance to your tune. But it'd be better just to make the implementation more complete in the solutions it finds. That's what we are working on now. Simon [1] http://research.microsoft.com/~simonpj/papers/assoc-types/index.htmhttp://research.microsoft.com/%7Esimonpj/papers/assoc-types/index.htm [2] http://research.microsoft.com/~simonpj/papers/gadthttp://research.microsoft.com/%7Esimonpj/papers/gadt ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users ___ Glasgow-haskell-users mailing list Glasgow-haskell-users@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
Re: Type checker loops with type families, overlapping and undecidable instances
The interaction between solving class constraints and equalities with type
families is currently rather ad hoc.
FYI
*September 2008*
*Unified Type Checking for Type Classes and Type Families*, T. Schrijvers,
M. Sulzmann. Presented at the ICFP 2008 poster session
(pdf available on Tom's homepage).
We propose to encode type class solving as type function solving. Earlier, I
suggested
the opposite direction. Either way works and leads to a system which can
properly
deal with any sort of type class and type function interaction plus can be
straightforwardly extended to support co-inductive type classes/functions.
-Martin
We are currently re-designing that interaction and may then make the
fixed-depth restriction more broadly applicable. However, as Tom already
mentioned, the cycle does not involve type families in your example anyway.
Manuel
José Pedro Magalhães:
Hello Lennart,
Yes, but according to the manual (
http://www.haskell.org/ghc/docs/latest/html/users_guide/type-class-extensions.html#undecidable-instances),
Termination is ensured by having a fixed-depth recursion stack. So I would
expect at least termination, which I'm not getting (but I guess that can be
due to the type families).
Thanks,
Pedro
On Thu, Dec 4, 2008 at 15:10, Lennart Augustsson [EMAIL PROTECTED]wrote:
Turning on UndecidableInstances is the same as saying: OK typechcker,
you can loop if I make a mistake.
I've not looked closely at your code, but if you turn on that flag,
looping is probably not a bug.
-- Lennart
2008/12/4 José Pedro Magalhães [EMAIL PROTECTED]:
Hello all,
Please consider the following code:
{-# OPTIONS -Wall #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances#-}
{-# LANGUAGE TypeOperators#-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
module Test where
-- Some view
class Viewable a where
type View a
to :: a - View a
-- Structural representations
data Unit= Unit
data a :+: b = L a | R b
instance Viewable Unit where
type View Unit = Unit
to = id
instance (Viewable a, Viewable b) = Viewable (a :+: b) where
type View (a :+: b) = a :+: b
to = id
-- Worker class
class F' a where
f' :: a - ()
instance F' Unit where
f' Unit = ()
instance (F a, F b) = F' (a :+: b) where
f' (L x) = f x
f' (R x) = f x
-- Dispatcher class
class (Viewable a, F' (View a)) = F a where
f :: a - ()
f = f' . to
instance F Unit where
f = f'
instance (F a, F b) = F (a :+: b) where
f = f'
-- All generic instances
instance (Viewable a, F' (View a)) = F a
-- A recursive datatype
data Nat = Zero | Succ Nat
-- Instance of Viewable
instance Viewable Nat where
type View Nat = Unit :+: Nat
to = undefined
-- Uncommenting the line below causes the typechecker to loop (GHC
6.10.1,
Windows)
--test = f Zero
Is this expected behavior or a bug?
Thanks,
Pedro
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
___
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
