>
> Sorry for the late reply. Thanks Oleg, I take it the Northern hemisphere is now on academic summer holidays. > > [snip] > > > Finally, I still think most of the "magic" in everything > > we've been talking about boils down to being able to > > have a type variable that can take on any type *except* > > a certain handful. This would allow us to avoid > > overlapping instances of both classes and type families, > would allow us to define TypeEq, etc. Moreover, it would > > be a more direct expression of what programmers intend, > > and so make code easier to read. Such a constraint > cannot be part of the context, because > > Alas, such `type variables' with inequality constraints > are quite complex, and the consequences of their > introduction are murky. Let me illustrate. First of all, > the constraint /~ (to be used as t1 /~ Int) doesn't help > to define TypeEq, etc. because constraints are not used > when selecting an instance. ... Yes indeed we can't use constraints when selecting an instance, several posters have pointed this out. I've suggested we call these inequality 'restraints' rather than 'constraints'. And a different syntax has been proposed, similar to pattern guards: type instance TypeEq a b | a /~ b = HTrue > Instances are selected only by > matching a type to the instance head. Instance selection > based on constraints is quite a change in the type checker > , and is unlikely to be implemented. I agree that selecting instances based on constraints would be abig change, but ... Selecting instances based on inequalities is already implemented in GHC and Hugs. (And has been successfully used for over a decade.) You've used it extensively yourself in the HList work, and much other type-level manipulation (such as IsFunction). Unfortunately, it's not called 'instance selection based on inequalities' (or some such), and its implementation got all mixed up with Functional Dependencies, which to my mind is an orthogonal part of the design. Instance selection based on inequalities is called 'Overlapping Instances'. The difficulty in adopting it into Haskell prime is that it isn't thoroughly specified, and you can currently only use it with FunDeps. To avoid confusion with FunDeps, let's imagine we could use overlapping instances with Type Families: type family HMember e l type instance HMember a HNil = HFalse type instance HMember a (HCons a l') = HTrue type instance HMember a (HCons b l') = HMember a l' Selecting that last instance implies a /~ b. (Otherwise the HTrue instance would be selected). Using inequality restraints, we'd write that last instance as: type instance HMember a (HCons b l') | a /~ b = HMember a l' And by putting an explicit inequality we are in fact avoiding the trouble with overlaps and all their implicit logic: The compiler can check that although the instance heads do overlap, the inequality disambiguates the instances. So type inference could only select one instance at most. I think this could be implemented under the new OutsideIn(X) type inference: Inference for the ordinary instances proceeds as usual. Inequalities give rise to implication terms(as used for GADTs), with the inequality in the antecedent: (a /~ b) implies (TypeEq a b ~ HFalse) As with GADTs, inference needs evidence that a /~ b before applying the consequent. There is no danger of clashing with other instances of TypeEq, because the instance (including inequality) doesn't overlap any of them. (I made some long posts to the Haskell-prime list last month, explaining in more detail, and responding to your TTypeable suggestion.) > > _______________________________________________ > 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 |
Let me see if I understand the different points of view. You advocate keeping Overlapping Instances, with changes to instance resolution algorithm. I advocate abolishing Overlapping Instances, claiming it results in no loss of expressiveness. In my approach, the changes in GHC are minor (essentially bug fixing and a matter of pretty-printing), not involving the algorithms of instance resolution. Incidentally, I have advocated abolishing Overlapping Instances in a short presentation at the 2004 Haskell Workshop (almost immediately after Ralf's HList talk). > Selecting instances based on inequalities is already implemented in > GHC and Hugs. (And has been successfully used for over a decade.) > You've used it extensively yourself in the HList work, and much other > type-level manipulation (such as IsFunction). I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping instances, and indeed _some_, simple code using overlapping instances work the same way in GHC and Hugs. However, HList in full does not work in Hugs; while investigating the matter we have found many dark corners of the Overlapping Instances implementation in Hugs; Ralf has even found an example where the order of the constraints within a type mattered. After that we just abandoned Hugs. This fact constructively proves that implementation of overlapping instances is tricky; since there is no meta-theory, it is even hard to tell what is right. I don't think Overlapping Instances will be in Haskell' any time soon since there are doubts about the soundness. Overlapping instances are clearly unsound with type functions. Whether they are sound with functional dependencies is not clear, but there are warning signs: http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html Please see the whole discussion on Haskell-Cafe in July 2010. > I think this could be implemented under the new OutsideIn(X) > type inference: I should point out the need to extend the type inference algorithm (and prove that the extension is sound) on your point of view. My proposal does not affect the instance resolution algorithm at all. > I take it the Northern hemisphere is now on academic summer holidays. Generally, yes. I wish I had a holiday though... _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
Friends
This has been an interesting thread, but I've been on holiday, and been busy bug-fixing etc, so my cache is very cold. Moreover, I remember that there was much of it that I wasn't following anyway. It's tricky. So, let me ask: does anyone (eg Oleg) have concrete proposals on the table for things they'd like GHC to do? Arising from the thread, two particular things jump out at me. I'm not planning to do anything immediate about either of them. 1. Support for type representations. Oleg showed this: | I have implemented type-level TYPEREP (along with a small library for higher-order | functional programming at the type level). Overlapping instances may indeed be | avoided. The library does not use functional dependencies either. | | http://okmij.org/ftp/Haskell/TTypeable/ Yesterday, Brent, Stephanie, Dimitrios, Julien and I were talking about better support for type reps too, something like a better Typeable class: class BetterTypeable a where typeOf :: Proxy a -> BetterTypeRep a data Proxy a The "better" part is that - Both BetterTypeable and Proxy could be poly-kinded, so we didn't need Typeable1, Typeable2 etc - BetterTypeRep is type-indexed (unlike the current TypeRep) But BetterTypeRep is still a value-level thing. You want a type-level type representation, for reasons I don't yet understand. In any case, *some* built in support for getting at type reps seems reasonable; the question is exactly what. 2. Support for overlapping type function equations. There seems no reason in principle to disallow type instance F where F Int = Bool F a = [a] There is overlap, but it is resolved top-to-bottom. The only real difficulty with this is how to render it into FC. The only decent way seems to me to be to allow FC axioms to do pattern matching themselves. So the FC rendering might be ax32 a = case a of Int -> F Int ~ Bool _ -> F a ~ [a] That is, the axioms become type-indexed. I don't know what complications that would add. Simon | -----Original Message----- | From: [hidden email] [mailto:[hidden email]] On | Behalf Of [hidden email] | Sent: 28 July 2011 06:28 | To: [hidden email] | Cc: [hidden email]; haskell- | [hidden email] | Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level recursion | | | Let me see if I understand the different points of view. You advocate | keeping Overlapping Instances, with changes to instance resolution | algorithm. I advocate abolishing Overlapping Instances, | claiming it results in no loss of expressiveness. In my approach, the | changes in GHC are minor (essentially bug fixing and a matter of | pretty-printing), not involving the algorithms of instance | resolution. Incidentally, I have advocated abolishing Overlapping | Instances in a short presentation at the 2004 Haskell Workshop (almost | immediately after Ralf's HList talk). | | > Selecting instances based on inequalities is already implemented in | > GHC and Hugs. (And has been successfully used for over a decade.) | > You've used it extensively yourself in the HList work, and much other | > type-level manipulation (such as IsFunction). | | I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping | instances, and indeed _some_, simple code using overlapping | instances work the same way in GHC and Hugs. However, HList in | full does not work in Hugs; while investigating the matter we have | found many dark corners of the Overlapping Instances | implementation in Hugs; Ralf has even found an example where the order of | the constraints within a type mattered. After that we just abandoned | Hugs. This fact constructively proves that implementation of | overlapping instances is tricky; since there is no meta-theory, it is | even hard to tell what is right. | | I don't think Overlapping Instances will be in Haskell' any time soon | since there are doubts about the soundness. Overlapping | instances are clearly unsound with type functions. Whether they are | sound with functional dependencies is not clear, but there are warning | signs: | | http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html | | Please see the whole discussion on Haskell-Cafe in July 2010. | | > I think this could be implemented under the new OutsideIn(X) | > type inference: | I should point out the need to extend the type inference algorithm | (and prove that the extension is sound) on your point of view. My | proposal does not affect the instance resolution algorithm at all. | | | > I take it the Northern hemisphere is now on academic summer holidays. | Generally, yes. I wish I had a holiday though... | | | _______________________________________________ | 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 |
> But BetterTypeRep is still a value-level thing. You want a type-level > type representation, for reasons I don't yet understand. > > 2. Support for overlapping type function equations. I'd like to have type-level type representations to _implement_ overlapping type function equations. With type level Typeable, you would not need to do anything about point 2 therefore. The problem 2 will be solved. > There seems no reason in principle to disallow > type instance F where > F Int = Bool > F a = [a] I would implement this as follows: > type instance F x = F' (EQ (TYPEOF x) INT) x > type family F' trep x > type instance F' TRUE x = Bool > type instance F' FALSE x = [x] Furthermore, type-level Typeable is possible already, although in quite an ugly way: your can read INT as a Peano numeral, and EQ as Peano numeral equality. In fact, I have demonstrated such an implementation (even more complex case, for higher-kinds): http://okmij.org/ftp/Haskell/TTypeable/ > That is, the axioms become type-indexed. I don't know what > complications that would add. With TTypeable, none of that would be needed. Overlapping Instances just become redundant. > So, let me ask: does anyone (eg Oleg) have concrete proposals on the > table for things they'd like GHC to do? First of all, can something be done about the behavior reported by David and discussed in the first part of the message http://www.haskell.org/pipermail/haskell-prime/2011-July/003489.html That is, if *no* undecidable instances are used, the type checker should reduce type functions for as long as needed. No context restrictions should be used. Second, what is the status of Nat kinds and other type-level data that Conor was/is working on? Nat kinds and optimized comparison of Nat kinds would be most welcome. Type level lists are better still (relieving us from Goedel-encoding type representations). Would it be possible to add TYPEREP (type-level type representation) as a kind, similar to that of natural numbers and booleans? Finally, could GHC automatically derive instances of TTypeable, which maps types to TYPEREP: type family TTypeable (x :: *) :: TYPEREP Cheers, Oleg _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
Helllo,
On Sat, Jul 30, 2011 at 2:11 AM, <[hidden email]> wrote:
I did some work on adding a Nat kind to GHC, you can find the implementation in the "type-nats" branch of GHC. The code there introduces a new kind, Nat, and it allows you to write natural numbers in types, using singleton types to link them to the value level. The constraint solver for the type level naturals in that implementation is a bit flaky, so lately I have been working on an improved decision procedure. When ready, I hope that the new solver should support more operations, and it should be much easier to make it construct explicit proof objects (e.g., in the style of System FC).
-Iavor PS: I am going on vacation next week, so I'll probably not make much progress on the new solver in August. _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
By the way, I have been testing your type-nats branch this week. I
added my observations to the GHC trac ticket on the feature, as you probably saw. After a discussion with other people here at HacPhi, I've decided that what I'm going to attempt is to add type-level Maybes so that subtraction and other partial operations can exist. This entails adding Maybe as an arity-1 kind constructor, which of course means adding the notion of kind constructors that have nonzero arities at all. On Sat, Jul 30, 2011 at 1:55 PM, Iavor Diatchki <[hidden email]> wrote: > Helllo, > > On Sat, Jul 30, 2011 at 2:11 AM, <[hidden email]> wrote: >> >> Second, what is the status of Nat kinds and other type-level data that >> Conor was/is working on? Nat kinds and optimized comparison of Nat >> kinds would be most welcome. Type level lists are better still >> (relieving us from Goedel-encoding type representations). >> > > I did some work on adding a Nat kind to GHC, you can find the > implementation in the "type-nats" branch of GHC. The code there introduces > a new kind, Nat, and it allows you to write natural numbers in types, using > singleton types to link them to the value level. The constraint solver for > the type level naturals in that implementation is a bit flaky, so lately I > have been working on an improved decision procedure. When ready, I hope > that the new solver should support more operations, and it should be much > easier to make it construct explicit proof objects (e.g., in the style of > System FC). > -Iavor > PS: I am going on vacation next week, so I'll probably not make much > progress on the new solver in August. > _______________________________________________ > Haskell-prime mailing list > [hidden email] > http://www.haskell.org/mailman/listinfo/haskell-prime > > -- Dan Knapp "An infallible method of conciliating a tiger is to allow oneself to be devoured." (Konrad Adenauer) _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
| GHC trac ticket on the feature, as you probably saw. After a
| discussion with other people here at | HacPhi, I've decided that what I'm going to attempt is to add | type-level Maybes Hang on! Julien Cretin (from INRIA) is doing an internship here at Cambridge with Dimitrios and me. The primary goal is to support *typed* type-level programming; that is, to add a proper kind system to GHC. Broadly our approach is like Conor's SHE system, with minor syntactic differences. So type-level Maybes will appear automatically, as a special case, so it's probably a bit of a waste to implement them separately. There'll also be support for poly-kinded type-level functions, of course. The stuff will be on a branch in the main ghc repo soon. Julien: we should start a wiki page (see http://hackage.haskell.org/trac/ghc/wiki/Commentary, and look for the link to "Type level naturals"; one like that). On the wiki you should * add a link to the latest version of our (evolving) design document. * specify the branch in the repo that has the stuff * describe the status Iavor's stuff is still highly relevant, because it involves a special-purpose constraint solver. But Iavor's stuff is no integrated into HEAD, and we need to talk about how to do that, once you are back from holiday Iavor. Simon _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
In reply to this post by oleg-30
Oleg
| > There seems no reason in principle to disallow | > type instance F where | > F Int = Bool | > F a = [a] | | | I would implement this as follows: | | > type instance F x = F' (EQ (TYPEOF x) INT) x | > type family F' trep x | > type instance F' TRUE x = Bool | > type instance F' FALSE x = [x] But you have just pushed the problem off to the definition of EQ. And your definition of EQ requires a finite enumeration of all types, I think. But * is open, so that's hard to do. What you want is type instance EQ where EQ a a = TRUE EQ _ _ = FALSE and now we are back where we started. Moreover, encoding the negative conditions that turn an arbitrary collection of equations with a top-to-bottom reading into a set of independent equations, is pretty tedious. | First of all, can something be done about the behavior reported by | David and discussed in the first part of the message | | http://www.haskell.org/pipermail/haskell-prime/2011-July/003489.html OK. Can you give a small standalone test case to demonstrate the problem, and open a Track ticket for it? | Second, what is the status of Nat kinds and other type-level data that | Conor was/is working on? Julien is working hard on an implementation right now. The Wiki page is here http://hackage.haskell.org/trac/ghc/wiki/GhcKinds Attached there are documents describing what we are up to. | Would it be possible to add TYPEREP (type-level type representation) | as a kind, similar to that of natural numbers and booleans? Yes! See 5.4 of "the theory document". It's still very incoherent, but it's coming along. Simon _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
> But you have just pushed the problem off to the definition of EQ. And > your definition of EQ requires a finite enumeration of all types, I > think. But * is open, so that's hard to do. What you want is > type instance EQ where > EQ a a = TRUE > EQ _ _ = FALSE > and now we are back where we started. Not at all. In the first approximation, EQ is the _numerical_ equality, equality of two type-level naturals. Since Goedel numbering is no fun in practice, I agree on the second approximation, described in TTypeable.hs. I quote the beginning of that file for reference: > module TTypeable where > {- > It helps in understanding the code if we imagine Haskell had > algebraic data kinds. We could then say > > kind TyCon_name -- name associated with each (registered) type constructor > > kind NAT -- Type-level natural numbers > kind BOOL -- Type-level booleans > > kind LIST a = NIL | a :/ LIST a > > -- Type-level type representation > kind TYPEREP = (TyCon_name, LIST TYPEREP) > -} > > -- Type-lever typeOf > -- The more precise kind is * -> TYPEREP > type family TYPEOF ty :: * > > -- Auxiliary families > > -- The more precise kind is TyCon_name -> NAT > type family TC_code tycon :: * > > -- Sample type reps (the rest should be derived, using TH, for example) > -- Alternatively, it would be great if GHC could provide such instances > -- automatically or by demand, e.g., > -- deriving instance TYPEOF Foo > data TRN_unit > type instance TC_code TRN_unit = Z > type instance TYPEOF () = (TRN_unit, NIL) > data TRN_bool > type instance TC_code TRN_bool = S Z > type instance TYPEOF Bool = (TRN_bool, NIL) I could write a TH function tderive to be used as follows. When the user defines a new data type data Foo = ... then $(tderive ''Foo) expands in > data TRN_package_name_module_name_Foo > type instance TC_code TRN_package_name_module_name_Foo = > <very long type-level numeral that spells package_name_module_name_Foo in unary> > type instance TYPEOF Foo = (TRN_package_name_module_name_Foo, NIL) I think I can write such tderive right now. So, the EQ (or, TREPEQ as I call it) is defined in closed form: > -- Comparison predicate on TYPEREP and its parts > > -- TYPEREP -> TYPEREP -> BOOL > type family TREPEQ x y :: * > > type instance TREPEQ (tc1, targ1) (tc2, targ2) = > AND (NatEq (TC_code tc1) (TC_code tc2)) > (TREPEQL targ1 targ2) > > -- LIST TYPEREP -> LIST TYPEREP -> BOOL > type family TREPEQL xs ys :: * > > type instance TREPEQL NIL NIL = HTrue > type instance TREPEQL NIL (h :/ t) = HFalse > type instance TREPEQL (h :/ t) NIL = HFalse > type instance TREPEQL (h1 :/ t1) (h2 :/ t2) = > AND (TREPEQ h1 h2) (TREPEQL t1 t2) That is it. These are the all clauses. Again, I have already defined them, and it works in GHC 7.0. Certainly I would be grateful if GHC blessed them with a special attention so they run faster. _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
In reply to this post by Simon Peyton Jones
Hello,
On Tue, Aug 2, 2011 at 6:10 PM, Simon Peyton-Jones <[hidden email]> wrote: > Julien: we should start a wiki page (see http://hackage.haskell.org/trac/ghc/wiki/Commentary, and look for the link to "Type level naturals"; one like that). On the wiki you should > * add a link to the latest version of our (evolving) design document. > * specify the branch in the repo that has the stuff > * describe the status Yes, this would be quite useful! > Iavor's stuff is still highly relevant, because it involves a special-purpose constraint solver. But Iavor's stuff is no integrated into HEAD, and we need to talk about how to do that, once you are back from holiday Iavor. I'll send an e-mail to the list when I'm back. I think I've made quite a bit of progress on the solver, and I've been working on a document (actually a literate Haskell file) which explains how it works and also my understanding of GHC's constraint solver that I'd be very happy to get some feedback on. -Iavor _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
In reply to this post by oleg-30
<oleg@...> writes:
> > > [28 Jul 2011] ... . Incidentally, I have advocated abolishing Overlapping > Instances in a short presentation at the 2004 Haskell Workshop (almost > immediately after Ralf's HList talk). Hi Oleg, I appreciate it's been a very long time since this thread was active. But I think I might have discovered that you and Ralf were premature to reject overlaps w.r.t. HList. The headline news is that I have implemented hDeleteMany in Hugs. I'm dragging up this ancient history not to argue in favour of fundeps, nor to bring Hugs back from its slumbers, but pro a better-implemented approach to overlaps (preferably available with Type Families). To recap the context: > > > [AntC wrote] > > Selecting instances based on inequalities is already implemented in > > GHC and Hugs. (And has been successfully used for over a decade.) > > You've used it extensively yourself in the HList work, and much other > > type-level manipulation (such as IsFunction). Also the original post said: > > Selecting instances based on inequalities ... got all mixed up with > > Functional Dependencies ... > > I'm glad you mentioned Hugs. Indeed, Hugs implements overlapping > instances, and indeed _some_, simple code using overlapping > instances work the same way in GHC and Hugs. However, HList in > full does not work in Hugs; ... The point at which the HList paper "give up on persuading Hugs" was with the instance definitions for hDeleteMany [Section 6 'Ended up in murky water'] because "There is no real consensus on the overlapping instance mechanism as soon as functional dependencies are involved. ... Hugs reports that the instances are inconsistent with the functional dependency for HDeleteMany." There has been a lot of water under the bridge since that interchange. In particular, GHC has got type equality constraints mature, with powerful type inference. SPJ showed a technique he called "a functional-dependency-like mechanism (but using equalities) for the result type". [This was for an application where using an Associated Type would not work. So he introduced an extra type parameter to the class.] I noted that HList has an approximation to equality constraints (TypeCast). I took the fundep away from HDeleteMany, and instead implemented the instances with TypeCast constraints to infer the result type: 1. There's no longer trouble with fundep interference. 2. So you can declare the instances OK (with overlaps well-ordered). 3. The typecast works a dream. [To be precise, I haven't done away with fundeps altogether, because they support TypeCast. And I expect that hDeleteMany without fundeps is not going to play well with large-scale programs needing extensive type inference. My point is only that it's the interference between fundeps and overlap that messes up both.] We could possibly design a better fundep, but I think fundeps are moribund. I'd rather put the effort into introducing overlaps into Type Families, and addressing the soundness concerns. > > I don't think Overlapping Instances will be in Haskell' any time soon > since there are doubts about the soundness. Overlapping > instances are clearly unsound with type functions. Whether they are > sound with functional dependencies is not clear, but there are warning > signs: > > http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html > > Please see the whole discussion on Haskell-Cafe in July 2010. > I have now studied SPJ's post, and that whole discussion. [Heck, July 2010 had some heavy-duty type theory.] I note that one of the threads that month was on 'in-equality type constraint's -- which is exactly what I think it needs to handle overlapping instances in a disciplined way. SPJ's post is dense, and I think worth replying to in detail, now that we have mature experience with equality constraints. > > > I take it the Northern hemisphere is now on academic summer holidays. > Generally, yes. I wish I had a holiday though... > My timing is again terrible: I suppose Northern Hemisphere academics are furiously ending their year and heading for the beach. AntC _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
AntC <anthony_clayden@...> writes:
> > <oleg@...> writes: > > > > The headline news is that I have implemented hDeleteMany in Hugs. > Yikes! I'd better post the code. This assumes all the usual HList infrastructure, especially class/method TypeCast as defined in-line per http://okmij.org/ftp/Haskell/typecast.html Works on Hugs version Sep 2006 -- yes! it's been hiding in plain view all these years. {- hDeleteMany does a type-indexed scan through an HList, removing all elements type `e`, even if they occur many times. Takes the standard HList idiom of 3 instances: - end of HList -- contains only HNil - HList's head contains the element of interest (HCons e l'') - HList's head not interesting, pass on (HCons e' l'') The 'interesting' instance overlaps the 'not interesting'. -} class HDeleteMany e l l' where -- no fundep hDeleteMany :: e -> l -> l' instance (TypeCast HNil l') => HDeleteMany e HNil l' where hDeleteMany e HNil = typeCast HNil -- must typeCast the result instance (HDeleteMany e l'' l') => HDeleteMany e (HCons e l'') l' where hDeleteMany e (HCons _ l'') = hDeleteMany e l'' instance (HDeleteMany e l'' l''', TypeCast (HCons e' l''') l') => HDeleteMany e (HCons e' l'') l' where hDeleteMany e (HCons e' l'') = typeCast (HCons e' (hDeleteMany e l'')) -- tests: somelist = HCons True $ HCons 'H' $ HCons "HList" $ HCons (5 :: Int) HNil somemanylist = HCons "hello" $ HCons False somelist unmanylist = hDeleteMany "bye" (hDeleteMany (undefined :: Bool) somemanylist ) -- unmanylist ===> HCons 'H' (HCons 5 HNil) AntC _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
In reply to this post by Simon Peyton Jones
Simon Peyton-Jones <simonpj@...> writes:
> [from 29 Jul 2011] > > So, let me ask: does anyone (eg Oleg) have concrete proposals on the table for things they'd like GHC to do? > > Arising from the thread, two particular things jump out at me. ... The two things are, I think, trying to achieve the same objective. Namely, supporting type-level inference driven from a type-level equality predicate. Of those two things (details continued below), I understand Oleg does have a concrete proposal for the first (and a prototype). My proposal earlier in the thread was along the lines of your second particular thing. But I delayed replying immediately: - Oleg suggested I refer back to several similar threads in July 2010 (thank you, that was indeed a valuable discussion) - GHC has now delivered robust type inference with type equality constraints, - and superclass constraints. - And we have the beginnings of data Kinds - And there has been 'loose talk' of closed Kinds (To explain that last: I believe the type inference for closed Kinds will need a similar mechanism to overlapping instances for TypeFamilies.) Although this thread is titled FunctionalDependencies, I'm not going to say anything about them except that they interfere badly with overlaps, so both have got an unfair reputation IMHO. Thanks to the improvements in type inference, SPJ has shown a technique he called "a functional-dependency-like mechanism (but using equalities) for the result type". That applies for Type Class instances, and GHC supports overlapping for those, so I've used the technique to simulate overlapping TypeFamily instances. > > 1. Support for type representations. Oleg showed this: > > | I have implemented type-level TYPEREP ... > > > 2. Support for overlapping type function equations. > > There seems no reason in principle to disallow > type instance F where > F Int = Bool > F a = [a] > There is overlap, but it is resolved top-to-bottom. The only real > into FC. The only decent way seems to me to be to allow FC axioms to do pattern matching themselves. So the FC > rendering might be > ax32 a = case a of > Int -> F Int ~ Bool > _ -> F a ~ [a] > That is, the axioms become type-indexed. I don't know what complications that would add. > I favour support for overlapping type function equations, but not exactly that approach. I think a major complication from the programmer's point of view is that the type function equations would have to be declared all in the same place. (I suspect there would be a similar restriction with closed Kinds.) A complication for type inference is carrying around some representation of that case statement, and applying the top-to-bottom inference. I think it preferable from a programmer's point of view to have separately declared stand-alone instances. And I guess this might be easier to manage for type inference. And I propose a form for the instances that achieves the type function above, but with what you might call "explicitly non-overlapping overlaps", like this: type instance F Int = Bool type instance F a | a /~ Int = [a] -- explicit dis-equality restraint These can't overlap, because the restraint (aka type-level guard) says "you must have evidence that typevar a is not Int before this binding applies". And we can validate those instances for non-overlap: the instance heads overlap just in case a ~ Int. (I suspect much of this logic is already in place to handle overlapping instances. In a 2010 post Oleg gave a very convincing characterisation.) [Something very similar to dis-equality guards was briefly shown in Sulzmann & Stuckey. A Theory of Overloading (2002).] I'm calling these "restraints" because they're not like constraints. Restraints block instance matching, whereas constraints validate the instance _after_ matching. But the terminology is going to get confusing, because inside type inference, I think they'd be implemented as what's called "implication constraints" (as used for GADT's). That second binding gives rise to an axiom: (a /~ Int ==> F a ~ [a]) -- using ==> for implication (The axiom for the first binding is as usual, no implication needed.) I dislike Oleg's TypeRep approach, because it brings in another layer of encoding. I think it would be simpler from a programmer's point of view to have types 'standing for themselves'. I prefer "explicitly non-overlapping overlaps" because the type function guards look and behave similarly to guards for function bindings. (But a significant difference is that type function instances must be mutually exclusive, and that's how come they can be declared stand-alone. The requirement to be mutually exclusive means we avoid all that trouble with IncoherentInstances and imported overlaps silently changing behaviour -- I would explain further, but this post has gone on long enough.) AntC _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
In reply to this post by oleg-30
<oleg@...> writes:
> I'd like to have type-level type representations to _implement_ > overlapping type function equations. With type level Typeable, you > would not need to do anything about point 2 therefore. The problem 2 > will be solved. > > > There seems no reason in principle to disallow > > type instance F where > > F Int = Bool > > F a = [a] > > I would implement this as follows: > > > type instance F x = F' (EQ (TYPEOF x) INT) x > > type family F' trep x > > type instance F' TRUE x = Bool > > type instance F' FALSE x = [x] > Thanks Oleg. I'm familiar with that style from HList, but it still seems cumbersome to me (compared to separate equations). I suppose a type-level if- then-else would be possible? Does this read any better? type instance F x = IF (EQ (TYPEOF x) INT) Bool [x] I note there by the way, that INT ~ (TYPEOF Int), is that upshifting the name going to work well for all Prelude types? How about (TYPEOF ()) or (TYPEOF [a])? The EQ seems somehow redundant. We can only test type (reps) for equality, or do you envisage inducing some ordering over typereps? How scalable is your approach with multi-argument type functions? Such as: module Mine where type family F a b data Mine = ... type instance F Mine Int = ... type instance F Mine y = ... -- overlap on 2nd arg module Yours where import Mine data Yours = ... type instance F Yours Bool = ... -- no overlap with F Mine b type instance F Yours y = ... -- overlap on 2nd arg We'd need a clan of helper functions F'Mine, F'Yours, etc. This multi-argument example also goes against closed type families, I think. > > Finally, could GHC automatically derive instances of TTypeable, which > maps types to TYPEREP: > type family TTypeable (x :: *) :: TYPEREP > I can see that if we went the route of type-level Typeable, it would need compiler support. But do we need that? Would it be sufficient to have a compiler-supported if-then-else type equality? Perhaps IFEQ, like this: type instance F a = IFEQ a Int Bool [a] type instance F a = (a ?~ Int) Bool [a] -- over-exotic syntax? To be fair to the design you've put into TTypeable, we'd also need to handle polymorphic/partly-ground/higher-ranked types: type instance G a = IFEQ a (Maybe b) b () type instance IsFunction a = IFEQ a (_ -> _) TRUE FALSE -- the classic type instance IsNum a = IFEQ a (Num b => b) a Int And that last example is a worry: what we're calling a type equality test is really a test for unifiability. AntC _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
In reply to this post by oleg-30
<oleg@...> writes:
> > > I don't think Overlapping Instances will be in Haskell' any time soon > since there are doubts about the soundness. Overlapping > instances are clearly unsound with type functions. Whether they are > sound with functional dependencies is not clear, but there are warning > signs: > > http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html > cafe http://www.haskell.org/pipermail/haskell-cafe/2012-May/101417.html ) As SPJ says there, I don't expect there's any real difference in the fundeps approach compared to type families. And as a matter of taste, I find type families more easy to understand and reason about, and more *functional*. But I don't see in SPJ's post any real doubts about soundness, just restrictions that would have to be imposed. He concludes "I believe that if ..., then overlap of type families would be fine." The only onerous restriction is that overlapping instances would have to be in a single module. And I don't think that is needed under my proposal to dis- overlap overlaps. As a matter of interest, how would the TTypeable approach address those examples? Particularly the existentials (examples 3 and 4). How would it look inside the GADTs to discharge the constraints (or apply the type functions)? I notice example 4 (and 1) 'exploits' separate compilation/imported overlapping instances to arrive at unsoundness. How does TTypeable handle imported instances? AntC _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms
(as yet unimplemented) Simon | -----Original Message----- | From: [hidden email] [mailto:haskell-prime- | [hidden email]] On Behalf Of AntC | Sent: 24 May 2012 14:00 | To: [hidden email] | Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level | recursion | | <oleg@...> writes: | | > | > | > I don't think Overlapping Instances will be in Haskell' any time soon | > since there are doubts about the soundness. Overlapping instances are | > clearly unsound with type functions. Whether they are sound with | > functional dependencies is not clear, but there are warning | > signs: | > | > http://www.haskell.org/pipermail/haskell-cafe/2010-July/080043.html | > | I have now worked through that post in detail, thank you. And replied | (on the cafe http://www.haskell.org/pipermail/haskell-cafe/2012- | May/101417.html ) | | As SPJ says there, I don't expect there's any real difference in the | fundeps approach compared to type families. And as a matter of taste, I | find type families more easy to understand and reason about, and more | *functional*. | | But I don't see in SPJ's post any real doubts about soundness, just | restrictions that would have to be imposed. He concludes "I believe that | if ..., then overlap of type families would be fine." | | The only onerous restriction is that overlapping instances would have to | be in a single module. And I don't think that is needed under my | proposal to dis- overlap overlaps. | | As a matter of interest, how would the TTypeable approach address those | examples? Particularly the existentials (examples 3 and 4). How would it | look inside the GADTs to discharge the constraints (or apply the type | functions)? | | I notice example 4 (and 1) 'exploits' separate compilation/imported | overlapping instances to arrive at unsoundness. How does TTypeable | handle imported instances? | | AntC | | | | _______________________________________________ | 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 |
Simon Peyton-Jones <simonpj@...> writes:
> > See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms > (as yet unimplemented) > > Simon > Thank you Simon (and Pedro). Are you inviting comment/suggestions/requests for clarification at this stage? (Or is this under-the-radar research?) There is plenty of prior work/similar ideas to include in the references. How's the best way to help? (Without unleashing a maelstrom.) AntC _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
Hi,
On Tue, May 29, 2012 at 11:03 AM, AntC <[hidden email]> wrote:
Definitely! I think the design space should be explored in detail. There is plenty of prior work/similar ideas to include in the references. That document is not a paper draft; it's a draft of a design of a new GHC extension. How's the best way to help? (Without unleashing a maelstrom.) Perhaps having a wiki page where the problem of OverlappingInstances is discussed, and alternative solutions are proposed, so that at some point we can look at all of them and try to make an informed decision. I think it's good to have a wiki page to guide this sort of email discussion. Cheers, Pedro
_______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
I have expanded the draft spec on http://hackage.haskell.org/trac/ghc/wiki/NewAxioms to answer some of the questions on AntC’s discussion page. From: [hidden email] [mailto:[hidden email]]
On Behalf Of José Pedro Magalhães Hi, On Tue, May 29, 2012 at 11:03 AM, AntC <[hidden email]> wrote: Simon Peyton-Jones <[hidden email]> writes: Thank you Simon (and Pedro).
_______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
Simon Peyton-Jones <simonpj@...> writes:
> > I have expanded the draft spec on > http://hackage.haskell.org/trac/ghc/wiki/NewAxioms Thanks Simon, that's much clearer. By the way, are the examples for the multi- type instance declarations quite as intended? The heads have no head, as it were. Did you mean, or is this allowed? type instance F [a] where ... type instance F (a, b) where ... (From a documentation point of view, this shows that the instance groups are non-overlapping.) > to answer some of the questions on AntC’s discussion page. > (I'd rather you called it just *the* discussion page; I'm doing the ego-less contributor thing. I must admit that after I got the page started, I've not had so much time to keep building it.) AntC _______________________________________________ Haskell-prime mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-prime |
Free forum by Nabble | Edit this page |