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: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On | Behalf Of oleg@okmij.org | Sent: 28 July 2011 06:28 | To: anthony_clayden@clear.net.nz | Cc: mazieres-xb9592p9wenhvgjq5vnwdnd4be@temporary-address.scs.stanford.edu; haskell- | prime@haskell.org | 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 | Haskell-prime@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-prime

Helllo, On Sat, Jul 30, 2011 at 2:11 AM, 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.

| 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

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

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

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

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

Simon Peyton-Jones 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

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: haskell-prime-bounces@haskell.org [mailto:haskell-prime-bounces@haskell.org] On Behalf Of José Pedro Magalhães Sent: 29 May 2012 11:14 To: AntC Cc: haskell-prime@haskell.org Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level recursion Hi, On Tue, May 29, 2012 at 11:03 AM, AntC mailto:anthony_clayden@clear.net.nz> wrote: Simon Peyton-Jones mailto: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? 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 AntC _______________________________________________ Haskell-prime mailing list Haskell-prime@haskell.orgmailto:Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime

No I didn't intend to put more in the header, perhaps less. I've added more clarification. Simon | -----Original Message----- | From: haskell-prime-bounces@haskell.org [mailto:haskell-prime- | bounces@haskell.org] On Behalf Of AntC | Sent: 08 June 2012 02:00 | To: haskell-prime@haskell.org | Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level | recursion | | Simon Peyton-Jones 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 | Haskell-prime@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-prime

Yes, good point about idiom 1; I've added it. S | -----Original Message----- | From: haskell-prime-bounces@haskell.org [mailto:haskell-prime- | bounces@haskell.org] On Behalf Of AntC | Sent: 10 June 2012 06:23 | To: haskell-prime@haskell.org | Subject: Re: TypeFamilies vs. FunctionalDependencies & type-level | recursion | | Simon Peyton-Jones writes: | | > | > No I didn't intend to put more in the header, perhaps less. | > I've added more clarification. | > | > Simon | | Thanks Simon, I agree with keeping it terse; I agree with your "yuk" | rating for `of'. At risk of bikeshedding over surafce syntax (for a | feture that's still only a gleam in the eye) ... | | I think we're going to see two idioms for overlapping instances: | | Idiom 1: total instance (this would apply to all the HList examples). We | only need one instance group for the whole; then it's the type family | decl that seems superfluous. Perhaps we could allow: | | type family Equal a b :: Bool where | Equal a a = True | Equal a b = False | | type family HasMember a (b :: '[]) :: Bool where | HasMember a '[] = False -- (not | overlapping) | HasMember a ( a ': bs ) = True | HasMember a ( b ': bs ) = HasMember a bs | | Idiom 2: an instance group discriminated by the outermost type | constructor, or by one of the arguments (this might apply for Monad | Transformers). Then although the instance header is superfluous, it | might be useful documentation: | | module SomeLibrary where | type family F a b :: ... | | module MyModule where | data MyType = ... | type instance F MyType b where -- total function for a ~ | MyType | F MyType Int = ... | F MyType (Int, b) = ... | F MyType b = ... | | AntC | | | | | | _______________________________________________ | Haskell-prime mailing list | Haskell-prime@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-prime