RE: TypeFamilies vs. FunctionalDependencies type-level recursion
Yes, good point about idiom 1; I've added it. S | -Original Message- | From: haskell-prime-boun...@haskell.org [mailto:haskell-prime- | boun...@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 simonpj@... 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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
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-boun...@haskell.org [mailto:haskell-prime-boun...@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 anthony_clay...@clear.net.nzmailto:anthony_clay...@clear.net.nz wrote: Simon Peyton-Jones simonpj@...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 ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Hi, On Tue, May 29, 2012 at 11:03 AM, AntC anthony_clay...@clear.net.nz wrote: 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? 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.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: 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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
See also http://hackage.haskell.org/trac/ghc/wiki/NewAxioms (as yet unimplemented) Simon | -Original Message- | From: haskell-prime-boun...@haskell.org [mailto:haskell-prime- | boun...@haskell.org] On Behalf Of AntC | Sent: 24 May 2012 14:00 | To: haskell-prime@haskell.org | 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 | Haskell-prime@haskell.org | http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Hello, On Tue, Aug 2, 2011 at 6:10 PM, Simon Peyton-Jones simo...@microsoft.com 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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
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
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
| 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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Helllo, On Sat, Jul 30, 2011 at 2:11 AM, o...@okmij.org 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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
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 iavor.diatc...@gmail.com wrote: Helllo, On Sat, Jul 30, 2011 at 2:11 AM, o...@okmij.org 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 Haskell-prime@haskell.org 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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
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 Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Sorry for the late reply.
GHC does not accept the following program:
{-# LANGUAGE TypeFamilies #-}
x :: ()
x = const () (eq a b)
where
a :: S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z)
a = undefined
b :: S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z)
b = undefined
eq :: a - b - NatEq a b
eq _ _ = undefined
Notice that there are no undecidable instances required to compile
this function (or the portions of your TTypeable that this function
depends on). Yet GHC is still limiting my context stack (to 21 by
default). Obviously any kind of unicode encoding of type names is
going to run into the same sort of problem.
I would call this a bug, a recent one. Old versions of GHC (before
6.10, I think) imposed no context stack restrictions on programs with
decidable instances. Such a restriction is a recent addition (perhaps
introduced as a safe-guard since it was discovered that the old
versions of GHC did not properly implement the coverage condition). I
would recommend to file this as a bug, including the sample code
above. Your old message argues well why this new behavior should be
considered as a bug.
But now the comparison of types is depending on this context stack and
likely worsening the problem.
I agree that dependence on the arbitrary limit is unsatisfactory. That
is why I was hoping that Nat kinds will eventually make their way into
GHC (there are many arguments for their inclusion, and some people are
reportedly have been working on them).
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. 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.
Let us see how the selection based on mismatch could be implemented. To
recall, the constraint t1 ~ t2 means that there exists a
substitution on free type variables such that its application to t1
and t2 makes the types identical. In symbols,
\exists\sigma. t1\sigma = t2\sigma
We call the type t matches the instance whose head is th if
\exists\sigma. th\sigma = t
Now, we wish to define selection of an instance based on
dis-equality. We may say, for example, that the instance with the head
th is selected for type t if
\not\exists\sigma. th\sigma = t
In other words, we try to match t against th. On mismatch, we
select the instance. Let us attempt to define TypeEq
class TypeEq a b c | a b - c
instance TypeEq x x True
instance TypeEq x (NOT x) False
and resolve (TypeEq Int Bool x). We start with Bool: Bool matches x,
so the second instance cannot be selected. The first instance can't be
selected either. Thus, we fail. One may say: we should have started by
matching Int first, which would instantiate x. Matching Bool against
so instantiated x will fail, and the second instance will be
selected. The dependence on the order of matching leaves a bad
taste. It is not clear that there is always some order; it is not
clear how difficult it is to find one. I submit that introducing
disequality selection is quite a subtle matter. The TTypeable approach
was designed to avoid large changes in the type checker.
If you attend the Haskell implementors workshop, you might wish to
consider giving a talk about overlapping instances and the ways to get
around them or implement properly.
About dynamic loading [perhaps this should be moved in a separate
thread?]
I wish I knew ML better, but from looking at that paper, I can't
figure out the key piece of information, which is how to detect
overlapping type instance declarations. (Does ML even have something
equivalent?)
ML does not have type-classes; they can easily be emulated via dictionary
passing. Also, local open (recently introduced in OCaml) suffices
quite frequently, as it turns out.
I admit though I don't fully understand the problem:
In the absence of type families, I'm okay using something like
haskell-plugins that returns Dynamic. ...
With type families, I'm at a loss to figure out how this could even
work. You would need to know have a runtime representation of every
type family
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Thu, 23 Jun 2011 00:40:38 -0700 (PDT),
o...@okmij.org wrote:
How would you make this safe for dynamic loading? Would you have to
keep track of all the package/module names that have been linked into
the program and/or loaded, and not allow duplicates? Is dynamic
unloading of code ever possible? Or at least is re-loading possible,
since that appears to be key for debugging web servers and such?
I must read up on Andreas Rossberg's work and check AliceML (which is,
alas, no longer developed) to answer the questions on safe dynamic
loading. AliceML is probably the most ambitious system to support
type-safe loading. See, for example
http://www.mpi-sws.org/~rossberg/papers/Rossberg%20-%20The%20Missing%20Link.pdf
and other papers on his web page. He now works at Google, btw.
I wish I knew ML better, but from looking at that paper, I can't
figure out the key piece of information, which is how to detect
overlapping type instance declarations. (Does ML even have something
equivalent?)
In the absence of type families, I'm okay using something like
haskell-plugins that returns Dynamic. In the absence of type
families, Safe Haskell ought to be able to guarantee that typereps are
all unique, making cast safe in such a situation. (Even if somehow
two different pieces of code end up with conflicting functional
dependencies, this may muck with the expected behavior of the program,
as I get a different method from the one I was expecting, but it won't
undermine type safety.) If there were a way to use Baars Swiestra
instead of Dynamic, that would be even better.
With type families, I'm at a loss to figure out how this could even
work. You would need to know have a runtime representation of every
type family that's ever been instantiated, and you would need to check
this against all the type families in the dynamic module you are
loading. That seems very complicated.
MetaOCaml by not doing anything about it, letting the garbage code
accumulate. It is hard to know when all the code pointers to a DLL
are gone. GC do not usually track code pointers. One has to modify
GC, which is quite an undertaking. I suppose one may hack around by
registering each (potential) entry point as a ForeignPointer, and do
reference counting in a finalizer. Since a DLL may produce lots of
closures, each code pointer in those closures should be counted as
an entry point.
It would be very cool to GC the code, but that's more than I'm hoping
for.
Finally, how do you express constraints in contexts using type
families? For example, say I wanted to implement folds over tuples.
With fundeps (and undecidable instances, etc.), I would use a proxy
type of class Function2 to represent the function:
Your code can be re-written to use type functions almost mechanically
(the method definitions stay the same -- modulo uncurrying, which I used
for generality). I admit there is a bit of repetition (repeating the
instance head). Perhaps a better syntax could be found.
This is great. And in fact I was almost sold on your idea, until I
realized that GHC does not accept the following program:
{-# LANGUAGE TypeFamilies #-}
x :: ()
x = const () (eq a b)
where
a :: S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z)
a = undefined
b :: S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(S(Z)
b = undefined
eq :: a - b - NatEq a b
eq _ _ = undefined
Notice that there are no undecidable instances required to compile
this function (or the portions of your TTypeable that this function
depends on). Yet GHC is still limiting my context stack (to 21 by
default). Obviously any kind of unicode encoding of type names is
going to run into the same sort of problem.
So we seem to have come full circle: Undecidable instances are
problematic because program compilation depends on this arbitrary
context stack depth parameter. One way to avoid UndecidableInstances
is to assign a unique type-level Nat to each type. But now the
comparison of types is depending on this context stack and likely
worsening the problem.
A few thoughts:
First, obviously if we went base 2 instead of unary for the encoding,
types would get a lot shorter. If we took a SHA-256 hash of the type
name and encoded it, we could then pick some default context depth
(e.g., 21 + 256) that would make this work most of the time.
Second, I believe it is kind of unfair of GHC to reject the above
program. Without UndecidableInstances, GHC ought to be able to figure
out that the type checker will terminate. Moreover, in the real
world, GHC only has a finite amount of time and memory, so there is no
difference between divergence and really big types. I can already
crash GHC by feeding it a doubly-exponential-sized type such as:
a = let f0 x = (x, x)
f1 x = f0 (f0 x)
f2 x = f1 (f1 x)
f3 x = f2 (f2 x)
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Hi Oleg, On Wed, Jun 22, 2011 at 09:36, o...@okmij.org wrote: the need to define a duplicate of the class (MonadState' in your example) bloats the code significantly. I'm quite puzzled at the statement. Is there really significant bloat? Let us count. As the first example, let's take class C a with N special instances, mutually non-overlapping instances, and one catch-all instance instance C a. We have N+1 instances total. With the technique in the earlier message, we define an auxiliary class C' a flag with N special and one catch-all instance, all non-overlapping. We then define one instance of the original class C, performing the dispatch. The additional cost: one class declaration and one instance. Is one extra class and one instance considered a bloat? The extra class is systematically derived from the original one (so, one could get TH to do the deriving). My problem is exactly with this unnecessary repetition. If the extra class can be systematically derived from the original code, then it shouldn't have to be specified. All I'm saying is that if we would want to have such a mechanism for replacing OverlappingInstances, then we should also come up with a way (possibly even involving new syntax) to make it intuitive to use. (We've done something similar for the new generics stuff, by introducing DefaultSignatures.) But I am still doubtful of the runtime performance of your code I believe discussing performance may be a bit premature; Perhaps, but this was prompted by your suggestion of considering deprecating OverlappingInstances. I have lots of code that relies on it, and I wouldn't want it to start triggering warnings just yet :-) Cheers, Pedro ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
| One thing you could do to help in this specific case would be to use a | different M1 tag--e.g., M1 S ... for selectors and M1 NS ... for | fields without selectors (or K1 NS). I presume you've already | considered this and/or it's too late to make such a change. (Or to | move the distinction up to the constructor with two different | constructor tags, CR and CN for record and no-record.) I don't think it's too late to make a change. The stuff has only just gone in, so it's still very malleable. There may be other considerations, but legacy code isn't one of them! Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Hi Oleg, On Tue, Jun 21, 2011 at 09:35, o...@okmij.org wrote: 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/ At a first glance, I think your TYPEOF encodes less information about types than the new generics Rep. By less I mean that one could get that information from Rep (which is derived automatically). Our generics do not, however, encode a type-level natural per type. This greatly simplifies type-level type equality. But I am still doubtful of the runtime performance of your code; also, the need to define a duplicate of the class (MonadState' in your example) bloats the code significantly. Cheers, Pedro ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Hi, 2011/6/21 Simon Peyton-Jones simo...@microsoft.com | One thing you could do to help in this specific case would be to use a | different M1 tag--e.g., M1 S ... for selectors and M1 NS ... for | fields without selectors (or K1 NS). I presume you've already | considered this and/or it's too late to make such a change. (Or to | move the distinction up to the constructor with two different | constructor tags, CR and CN for record and no-record.) I don't think it's too late to make a change. The stuff has only just gone in, so it's still very malleable. There may be other considerations, but legacy code isn't one of them! I suppose that could be changed, yes, but what exactly are we trying to solve here? One can already specify different behavior for constructors with/without named fields. Are we trying to avoid OverlappingInstances? Then yes, this might help, but I'm not sure this change alone would make all generic programming possible without OverlappingInstances. (Also, I always thought UndecidableInstances were more evil, in some sense, and this change does nothing to remove the use of UndecidableInstances for generic programming.) Cheers, Pedro ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Tue, 21 Jun 2011 00:35:46 -0700 (PDT),
o...@okmij.org wrote:
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/
This is pretty cool.
One question I have is why you need UndecidableInstances. If we got
rid of the coverage condition, would your code be able to work without
relying on contexts for instance selection?
Now I understand the reference to the ML paper. If you were to
implement this in GHC you would encode the TC_code as the packge,
module, and type name, letter by letter? (Or bit by bit since symbols
can contain unicode?) Or could you use interface hashes (or whatever
those hex numbers are when you run ghc-pkg -v)?
How would you make this safe for dynamic loading? Would you have to
keep track of all the package/module names that have been linked into
the program and/or loaded, and not allow duplicates? Is dynamic
unloading of code ever possible? Or at least is re-loading possible,
since that appears to be key for debugging web servers and such?
Finally, how do you express constraints in contexts using type
families? For example, say I wanted to implement folds over tuples.
With fundeps (and undecidable instances, etc.), I would use a proxy
type of class Function2 to represent the function:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
class Function2 f a b r | f a b - r where
funcall2 :: f - a - b - r
-- An example, to show something of class Show and put the result in
-- a list endo:
data PolyShows = PolyShows
instance (Show a) =
Function2 PolyShows ([[Char]] - [[Char]]) a ([[Char]] - [[Char]]) where
funcall2 _ start a = start . (show a :)
-- Define a class for folds, as well as an instance for each tuple size:
class TupleFoldl f z t r | f z t - r where
tupleFoldl :: f - z - t - r
instance TupleFoldl f z () z where
tupleFoldl _ z _ = z
instance (Function2 f z v0 r1, Function2 f r1 v1 r2) =
TupleFoldl f z (v0,v1) r2 where
tupleFoldl f z (v0,v1) = funcall2 f (funcall2 f z v0) v1
instance (Function2 f z v0 r1, Function2 f r1 v1 r2, Function2 f r2 v2 r3) =
TupleFoldl f z (v0,v1,v2) r3 where
tupleFoldl f z (v0,v1,v2) =
funcall2 f (funcall2 f (funcall2 f z v0) v1) v2
--
-- ... and so on ...
Now I can run:
tupleFoldl PolyShows (id::[String]-[String]) (1,2) []
[1,2]
In your case, how do I define an Apply instance equivalent to
PolyShows?
Moreover, the fundep code above depends on the Function2 constraints
to make things work out correctly. It also has the nice property that
ghc can figure out many of the types automatically. You have to
specify id's type, but ghc figures out the type of [], figures out the
return type, and deals with 1 and 2 being (Num a = a).
Now is it the case that to do this with TYPEREP, you have to add an
internal class to express the constraints, and just pass extra
arguments to the class in a wrapper function? Presumably you then
have a bunch of ~ constraints. Does the type inference work as well?
It's a bit more typing, but if you can do it without undecidable
instances, or even with undecidable instances but keeping a bounded
context stack depth, then it would definitely be worth it. With
fundeps and undecidable instances, if I use the default context stack
depth of 21, my left and right folds crap out at 10 and 13 element
tuples, respectively.
David
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Hi all, Concerning 2. combination with overlapping instances, you say The solution has been described already in the HList paper: provide something the typeOf at the type level. That is, assume a type function TypeOf :: * - TYPEREP. ... Incidentally Pedro's new deriving Generic stuff does derive a kind of type-level type representation for types, I think. It's more or less as described in their paper. http://www.dreixel.net/research/pdf/gdmh_nocolor.pdf I'm very excited about this new Representable class and have just started playing with it, so it is too early for me to say for sure. However, my initial impression is that this is going to make me want OverlappingInstances even more because of all the cool things you can do with recursive algorithms over the Rep types... Yes, most likely. I have a package defining a few generic functions and showing some example uses ( http://hackage.haskell.org/package/generic-deriving). There I use OverlappingInstances (and even UndecidableInstances). An initial issue I'm running into (and again, this is preliminary, maybe I'll figure out a way without OverlappingInstances) is in implementing a function to serialize Generic data types to JSON. If the Haskell data type has selectors (i.e., is a record), then I would like to serialize/unserialize the type as a JSON object, where the names of the selectors are the JSON field names. If the Haskell data type does not have selectors, then I would like to serialize it as a JSON array. Generic deriving gives me the conIsRecord function, but this is at the value level, and I want to do something different at the type level. For a record, I need a list of (String, Value) pairs, while for a non-record, I need a list of Values. This leads me to write code such as the following: class JSON1 a r | a - r toJSON1 :: a - r instance (JSON a) = JSON1 (S1 NoSelector (K1 c a)) [Value] where toJSON1 (M1 (K1 a)) = [toJSON a] instance (Selector x, JSON a) = JSON1 (S1 x (K1 c a)) [(String, Value)] where toJSON1 s@(M1 (K1 a)) = [(nameOf s undefined, toJSON a)] where nameOf :: S1 c f p - c - String nameOf _ c - selName c The key piece of magic I need here (and in so many other places) is to be able to do one thing at the type level if x is a particular type (e.g., NoSelector) or sometimes one of a small number of types, and to do something else if x is any other type. Right. I think this is often essential. Cheers, Pedro ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
| I'd like to summarize the relationship between functional dependencies | and type functions, and propose a solution that should get rid of | overlapping instances. The solution does not require messing with | System-FC. In fact, it can be implemented today (although | ungainly). A small bit of GHC support will be appreciated. This sounds good. I am keen to identify features that provide the expressiveness that you and David and others want. However my brain is small. Concerning 1. mutual dependencies I believe that equality superclasses provide the desired expressiveness. The code may not look quite as nice, but equality superclasses (unlike fundeps) will play nicely with GADTs, type families, etc. Do you agree? Concerning 2. combination with overlapping instances, you say The solution has been described already in the HList paper: provide something the typeOf at the type level. That is, assume a type function TypeOf :: * - TYPEREP. By the HList paper do you mean http://homepages.cwi.nl/~ralf/HList/? I see no TYPEREP in that paper. Do you think you might perhaps elaborate your proposed solution explicitly? Perhaps saying explicitly: - This is the support we need from GHC - This is how you can then code examples X,Y,Z I know that all of this is embedded variously in your past writings but I'm not very good at finding exactly the right bits and turning them into proposed features! Incidentally Pedro's new deriving Generic stuff does derive a kind of type-level type representation for types, I think. It's more or less as described in their paper. http://www.dreixel.net/research/pdf/gdmh_nocolor.pdf Thanks Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Fri, 17 Jun 2011 13:21:41 +, Simon Peyton-Jones wrote: Concerning 1. mutual dependencies I believe that equality superclasses provide the desired expressiveness. The code may not look quite as nice, but equality superclasses (unlike fundeps) will play nicely with GADTs, type families, etc. Do you agree? By equality superclasses, do you just mean being able to say a ~ b in a class context? If so, that is basically what you get by enabling fundeps and defining a class such as: class AssertEq a b | a - b, b - a instance AssertEq a a Unless I'm missing something, that is not sufficient to do a lot of things I would like to do, as those things require both OverlappingInstances and FunctionalDependencies (as well as UndecidableInstances). A good test would be whether superclasses let you eliminate N^2 mtl instances and do something equivalent to: instance (Monad m) = MonadState s (StateT s m) where get = StateT $ \s - return (s, s) put s = StateT $ \_ - return ((), s) instance (Monad (t m), MonadTrans t, MonadState s m) = MonadState s (t m) where get = lift get put = lift . put Superclass equality is crucial for type families, since you can't mention a class's own type function in its head, but are there other things they allow you do to? Concerning 2. combination with overlapping instances, you say The solution has been described already in the HList paper: provide something the typeOf at the type level. That is, assume a type function TypeOf :: * - TYPEREP. ... Incidentally Pedro's new deriving Generic stuff does derive a kind of type-level type representation for types, I think. It's more or less as described in their paper. http://www.dreixel.net/research/pdf/gdmh_nocolor.pdf I'm very excited about this new Representable class and have just started playing with it, so it is too early for me to say for sure. However, my initial impression is that this is going to make me want OverlappingInstances even more because of all the cool things you can do with recursive algorithms over the Rep types... An initial issue I'm running into (and again, this is preliminary, maybe I'll figure out a way without OverlappingInstances) is in implementing a function to serialize Generic data types to JSON. If the Haskell data type has selectors (i.e., is a record), then I would like to serialize/unserialize the type as a JSON object, where the names of the selectors are the JSON field names. If the Haskell data type does not have selectors, then I would like to serialize it as a JSON array. Generic deriving gives me the conIsRecord function, but this is at the value level, and I want to do something different at the type level. For a record, I need a list of (String, Value) pairs, while for a non-record, I need a list of Values. This leads me to write code such as the following: class JSON1 a r | a - r toJSON1 :: a - r instance (JSON a) = JSON1 (S1 NoSelector (K1 c a)) [Value] where toJSON1 (M1 (K1 a)) = [toJSON a] instance (Selector x, JSON a) = JSON1 (S1 x (K1 c a)) [(String, Value)] where toJSON1 s@(M1 (K1 a)) = [(nameOf s undefined, toJSON a)] where nameOf :: S1 c f p - c - String nameOf _ c - selName c The key piece of magic I need here (and in so many other places) is to be able to do one thing at the type level if x is a particular type (e.g., NoSelector) or sometimes one of a small number of types, and to do something else if x is any other type. Closed type families might do it. One question I should think about is whether a combination of open type families with safe dynamic loading (if this is possible) and closed type families would cover everything I need. You'd need to be able to do things like: -- Type-level if-then-else closed type family IfEq :: * - * - * - * - * type instance IfEq a b c d = d type instance IfEq a a c d = c You would also need to be able to dangle closed type families off of open ones. (I.e., type instance Foo ProxyType = MyClosedTypeFamily) I also can't quite figure out how to pass around ad-hoc polymorphic functions the way you can with proxy types and a class such as: class Function f a b | f a - b where funcall :: f - a - b David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
| By equality superclasses, do you just mean being able to say a ~ b | in a class context? Yes. Or (F a ~ b). | Unless I'm missing something, that is not sufficient to do a lot of | things I would like to do, as those things require both | OverlappingInstances and FunctionalDependencies (as well as | UndecidableInstances). Correct. Hence Oleg's second point 2. combination with overlapping instances. Oleg claims to have a good story here. I'd like to see how he uses it to solve your problem. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
| Is there a policy that only a proposal's owner can modify the wiki | page? Or that you have to be a member of the Haskell' committee? I'm not sure. Malcolm Wallace is chair at the moment; I'm ccing him. I have no idea: I neither set up the wiki, nor do I have any interesting admin rights for it. Regards, Malcolm ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
| class C a b | a - b where | foo :: a - b | foo = error Yo dawg. | | instance C a b where | | The instance 'C a b' blatantly violates functional dependency and | should not have been accepted. The fact that it was is a known bug in | GHC. The bug keeps getting mentioned on Haskell mailing lists | about every year. Alas, it is still not fixed. Here is one of the | earlier messages about it: | | http://www.haskell.org/pipermail/haskell-cafe/2007-March/023916.html Wait. What about instance C [a] [b] ? Should that be accepted? The Coverage Condition says no, and indeed it is rejected. But if you add -XUndecidableInstances it is accepted. It's just the same for instance C a b It is rejected, with the same message, unless you add -XUndecidableInstances. Do you think the two are different? Do you argue for unconditional rejection of everything not satisfying the Coverage Condition, regardless of flags? Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On Wed, Jun 15, 2011 at 3:25 AM, Simon Peyton-Jones simo...@microsoft.com wrote: Wait. What about instance C [a] [b] ? Should that be accepted? The Coverage Condition says no, and indeed it is rejected. But if you add -XUndecidableInstances it is accepted. This 'clearly' violates the functional dependency as well. However, I must admit, it surprises me that GHC or Hugs ever detected this, and I imagine there's no general way to detect 'acceptable' instances. Do you think the two are different? Do you argue for unconditional rejection of everything not satisfying the Coverage Condition, regardless of flags? One obvious difference from the instances that appear (depending on how smart you're pretending to be as a compiler) bad but are nevertheless okay is that these have no contexts. If you can detect that, then: instance C a b instance C [a] [b] clearly have multiple independent instantiations on both sides, and so the relation is clearly non-functional. A simple heuristic might be to reject those, but allow: instance (..., D .. b .., ...) = C a b trusting that the context determines b in the right way. Is this possibly what GHC used to do? Of course, that allows 'Show b = C a b' so it's pretty weak. A slightly more intelligent heuristic might be to see if the fundeps in the context determine b, but that sounds like it might be leaving the realm of what's checkable. -- Dan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Wed, 15 Jun 2011 10:36:46 +, Simon Peyton-Jones wrote: The issue doesn't even arise with type families: class MonadState m where type State m :: * instance MonadState m = MonadState (MaybeT m) where type State (MaybeT m) = State m So examples that fail the coverage condition in fundeps, but (as you argue) are ok because the context expresses the dependency, are sometimes just fine with type families. Sorry, I guess that specific example works. It's the other one (which saves the programmer from having to define N^2 instances) that can never work with type families. | Now if, in addition to lifting the coverage condition, you add | OverlappingInstances, you can do something even better--you can write | one single recursive definition of MonadState that works for all | MonadTrans types (along with a base case for StateT). This is far | preferable to the N^2 boilerplate functions currently required by N | monad transformers: | | instance (Monad m) = MonadState s (StateT s m) where | get = StateT $ \s - return (s, s) | | instance (Monad (t m), MonadTrans t, MonadState s m) = | MonadState s (t m) where | get = lift get | put = lift . put Why do you need the first instance? Isn't the second sufficient for (StateT s m) as well? No, because those are not the same get function. In other words, there's a Control.Monad.State.Class.get, and a Control.Monad.Trans.State.Lazy.get function. When you define the recursive instance, you want the former, while when you define the base case, you need the latter. (Also, in the base case, you don't want lift.) Not only can I not see any way to avoid the N^2 instances with TypeFamilies, but I can't imagine any extension ever making this possible without threatening type safety. (That's not saying much, of course, given that we're dealing with the imagination of a non-language-designer here.) But this gets to the heart of the TypeFamilies limitation that caused me to start this thread. I want to be able to write code like this: class (Monad m) = MonadState m where type MonadStateType m get :: m (MonadStateType m) put :: (MonadStateType m) - m () instance (Monad m) = MonadState (StateT s m) where type MonadStateType (StateT s m) = s get = StateT $ \s - return (s, s) put s = StateT $ \_ - return ((), s) instance (Monad (t m), MonadTrans t, MonadState m) = MonadState (t m) where type MonadStateType (t m) = MonadStateType m get = lift get put = lift . put but I see no hope of ever making this work, and the result if that we have to have a separate instance for every pair of monad transformers. One not very good suggestion would be to add something like: instance (Monad (t m), MonadTrans t, MonadState m) = MonadState (t m) | (t m) /~ (StateT s m) where Having closed, overlapping type families would also be a way to solve the problem. David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Tue, 14 Jun 2011 19:52:00 -0700 (PDT),
o...@okmij.org wrote:
Dan Doel wrote:
class C a b | a - b where
foo :: a - b
foo = error Yo dawg.
instance C a b where
The instance 'C a b' blatantly violates functional dependency and
should not have been accepted. The fact that it was is a known bug in
GHC. The bug keeps getting mentioned on Haskell mailing lists
about every year. Alas, it is still not fixed. Here is one of the
earlier messages about it:
http://www.haskell.org/pipermail/haskell-cafe/2007-March/023916.html
But Oleg, isn't what you are complaining about *exactly* the lifting
of the coverage condition, which is one of the explicit points of
-XUndecidableInstances? Are you advocating two separate switches for
lifting Paterson vs. Coverage?
What about the following code--do you think this should be illegal,
too?
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
class C a b c | a - b where
instance C (Maybe a) (Maybe b) (Maybe b) where
David
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Hello,
On Wed, Jun 15, 2011 at 10:49 AM, dm-list-haskell-pr...@scs.stanford.eduwrote:
At Wed, 15 Jun 2011 10:10:14 -0700,
Iavor Diatchki wrote:
Hello,
On Wed, Jun 15, 2011 at 12:25 AM, Simon Peyton-Jones
simo...@microsoft.com
wrote:
| class C a b | a - b where
| foo :: a - b
| foo = error Yo dawg.
|
| instance C a b where
Wait. What about
instance C [a] [b]
No, those two are not different, the instance C [a] [b] should also be
rejected because it violates the functional dependency.
But now you are going to end up rejecting programs like this:
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE UndecidableInstances #-}
class C a b | a - b
class D a b | a - b
instance (D a b) = C [a] [b]
And a lot of useful code (including HList) depends on being able to do
things like the above.
Nope, this program will not be rejected because b is in the FD closure of
a. This stuff used to work a few GHC releases back, and I think that
this is the algorithm used by Hugs.
A functional dependency on a class imposes a constraint on the valid class
instances (in a similar fashion to adding super-class constraints to a
class). In general, checking this invariant may be hard, so it is fine for
implementations to be incomplete (i.e., reject some programs that do
satisfy the invariant or, perhaps, fail to terminate in the process). OTOH,
I think that if an implementation accepts a program that violates the
invariant, then this is a bug in the implementation.
The general rule defining an FD on a class like C is the following
logical
statement:
forall a b1 b2. (C a b1, C a b2) = (b1 = b2)
And in fact b1 and b2 are equal, up to alpha-conversion. They are
both just free type variables.
No, this was intended to be a more semantic property. Here it is in
English:
For any three ground types a, b1, and b2, if we can prove that both C
a b1 and C a b2 hold, then b1 and b2 must be the same type. The
theory of functional dependencies comes from databases. In that context, a
class corresponds to the schema for a database table (i.e., what columns
there are, and with what types). An instance corresponds to a rule that
adds row(s) to the table. With this in mind, the rule that I wrote above
exactly corresponds to the notion of a functional dependency on a database
table.
-Iavor
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
There was an interesting thread on haskell-prime [1], about the relationship between functional dependencies and type families. This message is my attempt to summarise the conclusions of that thread. I'm copying other interested parties (eg Oleg, Dimitrios) [1] http://www.haskell.org/pipermail/haskell-prime/2011-May/003416.html 1. As things stand in GHC you can do some things with functional dependencies that you can't do with type families. The archetypical example is type equality. We cannot write type family Eq a b :: * type instance Eq k k = True type instance Eq j k = False because the two instances overlap. But you can with fundeps class Eq a b c | a b - c instance Eq k k True instance Eq j k False As Alexey mentioned, fundeps have other disadvantages, so it's reasonable to ask whether type families could extend to handle cases like this. 2. In a hypothetical extension to type families, namely *closed* type families, you could support overlap: closed type family Eq a b :: * where type instance Eq k k = True type instance Eq j k = False The idea is that you give all the equations together; matching is top-to-bottom; and the type inference only picks an equation when all the earlier equations are guaranteed not to match. So there is no danger of making different choices in different parts of the program (which is what gives rise to unsoundness). 3. Closed type families are not implemented yet. The only tricky point I see would be how to express in System FC the proof that earlier equations don't match. Moreover, to support abstraction one might well want David's /~ predicate, so that you could say f :: forall a b. (a /~ b) = ..blah.. This f can be applied to any types a,b provided they don't match. I'm frankly unsure about all the consequences here. 4. As Roman points out, type families certainly do support recursion; it's just they don't support overlap. 5. David wants a wiki page fixed. But which one? And how is it locked down? 6. There is a very old Trac wiki page about total type families here http://hackage.haskell.org/trac/ghc/wiki/TypeFunctions/TotalFamilies Written by Manuel, I think it needs updating. That's my summary! Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On Tue, Jun 14, 2011 at 4:40 PM, Dan Doel dan.d...@gmail.com wrote:
On Tue, Jun 14, 2011 at 5:36 AM, Simon Peyton-Jones
simo...@microsoft.com wrote:
There was an interesting thread on haskell-prime [1], about the relationship
between functional dependencies and type families. This message is my
attempt to summarise the conclusions of that thread. I'm copying other
interested parties (eg Oleg, Dimitrios)
[1] http://www.haskell.org/pipermail/haskell-prime/2011-May/003416.html
1. As things stand in GHC you can do some things with functional
dependencies that you can't do with type families. The archetypical example
is type equality. We cannot write
type family Eq a b :: *
type instance Eq k k = True
type instance Eq j k = False
because the two instances overlap. But you can with fundeps
class Eq a b c | a b - c
instance Eq k k True
instance Eq j k False
As Alexey mentioned, fundeps have other disadvantages, so it's reasonable to
ask whether type families could extend to handle cases like this.
Fundeps no longer allow this as of GHC 7, it seems. It causes the same
fundep violation as the case:
class C a b | a - b
instance C a R
instance C T U
Are you sure that worked before? The following still does anyhow:
{-# LANGUAGE MultiParamTypeClasses, OverlappingInstances,
FunctionalDependencies
, EmptyDataDecls, FlexibleInstances,
UndecidableInstances #-}
class TypeCast a b | a - b, b-a where typeCast :: a - b
class TypeCast' t a b | t a - b, t b - a where typeCast' :: t-a-b
class TypeCast'' t a b | t a - b, t b - a where typeCast'' :: t-a-b
instance TypeCast' () a b = TypeCast a b where typeCast x = typeCast' () x
instance TypeCast'' t a b = TypeCast' t a b where typeCast' = typeCast''
instance TypeCast'' () a a where typeCast'' _ x = x
data R
data T
data U
class C a b | a - b
instance TypeCast R b = C a b
instance TypeCast U b = C T b
In fact this is how IsFunction was implemented in 2005[1], and the
same transformation appears to work for the Eq class too.
If we allow TypeFamilies we can use (~) instead of the TypeCast hack,
fortunately.
[1] http://okmij.org/ftp/Haskell/isFunction.lhs
-- Andrea
for R /~ U. Which I find somewhat sensible, because the definitions
together actually declare two relations for any type:
Eq T T False
Eq T T True
and we are supposed to accept that because one is in scope, and has a
particular form, the other doesn't exist. But they needn't always be
in scope at the same time.
Essentially, GHC 7 seems to have separated the issue of type-function
overlapping, which is unsound unless you have specific conditions that
make it safe---conditions which fundeps don't actually ensure (fundeps
made it 'safe' in the past by not actually doing all the computation
that type families do)---from the issue of instance overlapping, which
is always sound at least. But if I'm not mistaken, type families can
handle these cases.
I'd personally say it's a step in the right direction, but it probably
breaks a lot of HList-related stuff.
-- Dan
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Tue, 14 Jun 2011 09:36:41 +, Simon Peyton-Jones wrote: 5. David wants a wiki page fixed. But which one? And how is it locked down? This page: http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies Currently under cons for FunctionalDependencies, it says: AssociatedTypes seem to be more promising. I proposed the following fix: AssociatedTypes seem to be more promising, but in their current form are not as general as FunctionalDependencies [link]. where the link points to this or another email thread. Is there a policy that only a proposal's owner can modify the wiki page? Or that you have to be a member of the Haskell' committee? At any rate, when I log into the Haskell' wiki, I don't get an Edit button. That's all I meant by locked down. David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On Tue, Jun 14, 2011 at 11:27 AM, Andrea Vezzosi sanzhi...@gmail.com wrote: class C a b | a - b instance C a R instance C T U Are you sure that worked before? 80% The following still does anyhow: data R data T data U class C a b | a - b instance TypeCast R b = C a b instance TypeCast U b = C T b In fact this is how IsFunction was implemented in 2005[1], and the same transformation appears to work for the Eq class too. If we allow TypeFamilies we can use (~) instead of the TypeCast hack, fortunately. So it does. instance (b ~ R) = C a b instance (b ~ U) = C T b Which is odd. I don't think there's a way to justify this working. Either the preconditions are being taken into account, in which case there is no reason for this to behave differently from: instance C a R instance C T U or the preconditions are not being taken into account (which is the type class way), in which case both of the qualified instances are illegal, because they declare instances C T b for all b (plus a constraint on the use), which violates the fundep. I've seen examples like this before, and I think what GHC ends up doing (now) is fixing the 'b' to whatever instance it needs first. But I don't think that's very good behavior. In this case it happens that it's impossible to use at more than one instance, but if you accept the instances, you're back to the questions of type soundness that are only evaded because fundeps don't actually use all the information they allegedly express. -- Dan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Tue, 14 Jun 2011 10:40:48 -0400,
Dan Doel wrote:
1. As things stand in GHC you can do some things with functional
dependencies that you can't do with type families. The archetypical example
is type equality. We cannot write
type family Eq a b :: *
type instance Eq k k = True
type instance Eq j k = False
because the two instances overlap. But you can with fundeps
class Eq a b c | a b - c
instance Eq k k True
instance Eq j k False
As Alexey mentioned, fundeps have other disadvantages, so it's reasonable
to ask whether type families could extend to handle cases like this.
Fundeps no longer allow this as of GHC 7, it seems. It causes the same
fundep violation as the case:
class C a b | a - b
instance C a R
instance C T U
You absolutely still can use FunctionalDependencies to determine type
equality in GHC 7. For example, I just verified the code below with
GHC 7.02:
*Main typeEq True False
HTrue
*Main typeEq (1 :: Int) (2 :: Int)
HTrue
*Main typeEq (1 :: Int) False
HFalse
As always, you have to make sure one of the overlapping instances is
more specific than the other, which you can do by substituting a
parameter c for HFalse in the false case and fixing c to HFalse using
another class like TypeCast in the context. (As contexts play no role
in instance selection, they don't make the instance any more
specific.)
While I don't have convenient access to GHC 6 right this second, I'm
pretty sure there has been no change for a while, as the HList paper
discussed this topic in 2004.
David
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE OverlappingInstances #-}
{-# LANGUAGE UndecidableInstances #-}
class TypeCast a b | a - b where
typeCast :: a - b
instance TypeCast a a where
typeCast = id
data HTrue = HTrue deriving (Show)
data HFalse = HFalse deriving (Show)
class TypeEq a b c | a b - c where
typeEq :: a - b - c
instance TypeEq a a HTrue where
typeEq _ _ = HTrue
instance (TypeCast HFalse c) = TypeEq a b c where
typeEq _ _ = typeCast HFalse
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Sorry about the double send, David. I forgot to switch to reply-all in the gmail interface. On Tue, Jun 14, 2011 at 11:49 AM, dm-list-haskell-pr...@scs.stanford.edu wrote: You absolutely still can use FunctionalDependencies to determine type equality in GHC 7. For example, I just verified the code below with GHC 7.02: *Main typeEq True False HTrue *Main typeEq (1 :: Int) (2 :: Int) HTrue *Main typeEq (1 :: Int) False HFalse As always, you have to make sure one of the overlapping instances is more specific than the other, which you can do by substituting a parameter c for HFalse in the false case and fixing c to HFalse using another class like TypeCast in the context. (As contexts play no role in instance selection, they don't make the instance any more specific.) While I don't have convenient access to GHC 6 right this second, I'm pretty sure there has been no change for a while, as the HList paper discussed this topic in 2004. Okay. I don't really write a lot of code like this, so maybe I missed the quirks. In that case, HList has been relying on broken behavior of fundeps for 7 years. :) Because the instance: instance TypeEq a b c violates the functional dependency, by declaring: instance TypeEq Int Int Int instance TypeEq Int Int Char instance TypeEq Int Int Double ... instance TypeEq Int Char Int instance TypeEq Int Char Char ... and adding the constraint doesn't actually affect which instances are being declared, it just adds a constraint requirement for when any of the instances are used. It appears I was wrong, though. GHC doesn't actually fix the instance for such fundeps, and the following compiles and runs fine: class C a b | a - b where foo :: a - b foo = error Yo dawg. instance C a b where bar :: Int bar = foo x baz :: Char baz = foo x so we're using an instance C String Int and an instance C String Char despite the fact that there's a functional dependency from the first argument to the second. -- Dan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Tue, 14 Jun 2011 12:31:47 -0400, Dan Doel wrote: Sorry about the double send, David. I forgot to switch to reply-all in the gmail interface. Okay. I don't really write a lot of code like this, so maybe I missed the quirks. In that case, HList has been relying on broken behavior of fundeps for 7 years. :) Because the instance: instance TypeEq a b c violates the functional dependency, by declaring: instance TypeEq Int Int Int instance TypeEq Int Int Char instance TypeEq Int Int Double No, these are not equivalent. The first one TypeEq a b c is just declaring an instance that works forall c. The second is declaring multiple instances, which, if there were class methods, could have different code. The second one is illegal, because given just the first two types, a and b, you cannot tell which instance to pick. class C a b | a - b where foo :: a - b foo = error Yo dawg. instance C a b where bar :: Int bar = foo x baz :: Char baz = foo x so we're using an instance C String Int and an instance C String Char despite the fact that there's a functional dependency from the first argument to the second. A functional dependency such as | a b - c d just guarantees that a and b uniquely determine the instance. Hence, it is okay to have class methods that do not mention type variables c and d, because the compiler will still know which instance to pick. Since your code only has one instance of class C, the unique instance is trivially guaranteed and the code is fine. In fact, your code is effectively the same as: class C a where foo :: a - b foo = error Yo dawg. instance C a where The same issues happen with type families. The following code is obviously illegal, because you have a duplicate instance of class C: class C a where type Foo a foo :: a - Foo a foo = error Yo dawg. instance C [Char] where type Foo [Char] = Int instance C [Char] where type Foo [Char] = Char On the other hand, though the compiler won't accept it, you could at least theoretically allow code such as the following: instance C [Char] where type Foo [Char] = forall b. () = b David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On Tue, Jun 14, 2011 at 1:19 PM, dm-list-haskell-pr...@scs.stanford.edu wrote: No, these are not equivalent. The first one TypeEq a b c is just declaring an instance that works forall c. The second is declaring multiple instances, which, if there were class methods, could have different code. The second one is illegal, because given just the first two types, a and b, you cannot tell which instance to pick. Then why am I not allowed to write: class C a b | a - b instance C T [a] without undecidable instances? GHC actually complains in that case that the coverage condition is violated. But it is a single well specified instance that works for all a. The answer is that such an instance actually violates the functional dependency, but UndecidableInstances just turns off the checks to make sure that fundeps are actually functional. It's a, trust me, switch in this case (not just a, my types might loop, switch). So I guess HList will still work fine, and UndecidableInstances are actually more evil than I'd previously thought (thanks for the correction, Andrea :)). A functional dependency such as | a b - c d just guarantees that a and b uniquely determine the instance. Hence, it is okay to have class methods that do not mention type variables c and d, because the compiler will still know which instance to pick. It specifies that a and b uniquely determine c and d, so the choice of instances is unambiguous based only on a and b. This is the basis for type level computation that people do with fundeps, because a fundep 'a b - c' allows one to compute a unique c for each pair of types. If it were just about variable sets determining the instance, then we could just list those. But I can write: class C a b c d | a b - c And it will actually be a, b and d that determine the particular instance, but just listing 'a b d', or using the fundep 'a b d - c' is wrong, because the fundep above specifies that there is a single choice of c for each a and b. So we could have: C Int Int Char Int C Int Int Char Double C Int Int Char Float but trying to add: C Int Int Int Char to the first three would be an error, because the first two parameters determine the third, rather than the first, second and fourth. Being allowed to elide variables from the types of methods is one of the uses of fundeps, and probably why they were introduced, but it is not what fundeps mean. On the other hand, though the compiler won't accept it, you could at least theoretically allow code such as the following: instance C [Char] where type Foo [Char] = forall b. () = b The fundep equivalent of this is not 'instance C [Char] b'. It is: instance C [Char] (forall b. b) except types like that aren't allowed in instances (for good reason in general). The closest you could come to 'instance C T b' would be something like: type instance F T = b except that is probably interpreted by GHC as being (forall b. b). -- Dan ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
RE: TypeFamilies vs. FunctionalDependencies type-level recursion
| http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies | | Currently under cons for FunctionalDependencies, it says: | | AssociatedTypes seem to be more promising. | | I proposed the following fix: | | AssociatedTypes seem to be more promising, but in their | current form are not as general as FunctionalDependencies | [link]. OK, that one. I've made that change. | Is there a policy that only a proposal's owner can modify the wiki | page? Or that you have to be a member of the Haskell' committee? I'm not sure. Malcolm Wallace is chair at the moment; I'm ccing him. Simon ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On 30/05/2011, at 00:55, dm-list-haskell-pr...@scs.stanford.edu wrote: I'm absolutely not advocating making overlapping instances (or, worse, overlapping types) part of Haskell', nor under the impression that the committee would ever consider doing so. I'm just pointing out that right now OverlappingInstances are the only way to do recursive programming at the type level, for the specific reasons I outlined. I hope that before FunctionalDependencies or TypeFamilies or any other type-level programming becomes part of Haskell', there is a way to differentiate base and recursive cases *without* overlapping instances. FWIW, I don't think this is really about type-level recursion. You can do recursive programming with type families: data Z data S n type family Plus m n type instance Plus Z n = n type instance Plus (S m) n = S (Plus m n) It's deciding type equality via overlapping instances that is problematic here. But, as others have pointed out, this is somewhat dodgy anyway. I suppose what you really want is something like this: data True data False type family Equal a b Where Equal a b ~ True if and only if a and b are known to be the same type and Equal a b ~ False if and only if they are known to be different types. You could, in theory, get this by defining appropriate instances for all type constructors in a program: type instance Equal Int Int = True type instance Equal Int [a] = False type instance Equal [a] Int = False type instance Equal [a] [b] = Equal a b ... But that's infeasible, of course. However, nothing prevents a compiler from providing this as a built-in. Arguably, this would be much cleaner than the solution based on fundeps and overlapping instances. Roman ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On 29.05.2011 22:59, David Mazieres wrote: But now you have overlapping type synonyms, which pose a safety threat where the more-specific instance is not in scope. Therefore, Haskell likely cannot be extended to accept code such as the above. No it could. Inconsistency arise from fact that it's not guaranted that all instances are known. Such guaranties are possible with closed type families. In such families instances could be added only in the same module with family declaration. Here is simplistic example: data HTrue data HFalse closed type family Equal a b :: * closed type instance a a = HTrue closed type instance a b = HFalse No more instances could be added. So type could be determined unambigously. In type level programming type families often meant to be closed but there is no explicit way to say that and it limit their expressiveness. Also closed type families could help with lack of injectivity. It could be untracktable though. One possible extension that *would* enable type-level recursive programming is the ability to constrain by inequality of types. I noticed GHC is on its way to accepting a ~ b as a constraint that types a and b are equal. If there were a corresponding a /~ b, then one might be able to say something like: instance HLookup k (HCons (k, v) l) where ... instance (h /~ (k, v), HLookup k l) = HLookup k (HCons h l) where ... I can't see how it change things. AFAIR instances selected only by their heads, contexts are not taken into account. Besides type inequality could be easily implemented with closed type families. See code above. Here is contrived example of usage: instance (Equal Thing Int ~ HFalse) = Whatever Thing P.S. Also I have suspicion that version with fundeps will behave badly if more instances are added in another module. ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On Sun, May 29, 2011 at 7:59 PM, David Mazieres dm-list-haskell-pr...@scs.stanford.edu wrote: One of the more disgusting but also powerful implications of FunctionalDependencies is that, in conjunction with OverlappingInstances and UndecidableInstances, you can do recursive programming at the type level. This has been (ab)used to do some cool things (e.g., HList, HaskellDB, OOHaskell). It would seem very strange to me if haskell-prime made the choice of fundeps/type families based on the behaviour with OverlappingInstances. I'm under the impression that Overlapping is generally considered one of the more controversial extensions, and on the LanguageQualities wiki page [1] it's explicitly given as an example of something which violates them. So not only is Overlapping not in the language, but I imagine there are many people (myself included) who would like to ensure it stays out. My personal opinion is that if Haskell wants a more complete facility for type-level programming, that should be addressed directly, instead of via creative abuse of the class system and related machinery. Ben [1]: http://hackage.haskell.org/trac/haskell-prime/wiki/LanguageQualities ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
On Sun, May 29, 2011 at 6:45 PM, Ben Millwood hask...@benmachine.co.uk wrote:
It would seem very strange to me if haskell-prime made the choice of
fundeps/type families based on the behaviour with
OverlappingInstances. I'm under the impression that Overlapping is
generally considered one of the more controversial extensions, and on
the LanguageQualities wiki page [1] it's explicitly given as an
example of something which violates them. So not only is Overlapping
not in the language, but I imagine there are many people (myself
included) who would like to ensure it stays out.
My personal opinion is that if Haskell wants a more complete facility
for type-level programming, that should be addressed directly, instead
of via creative abuse of the class system and related machinery.
It should also be noted: the fact that functional dependencies work
with overlapping instances, while type families don't is not really
inherent in functional dependencies, but is instead related to choices
about how functional dependencies work that differ from how type
families do. And mainly, this is because functional dependencies fail
to incorporate local information, meaning they fail to work
appropriately in various situations (for instance, matching on a GADT
may refine a type, but that new information may not propagate through
a fundep).
In my experience, you can construct examples that should lead to type
soundness issues with fundeps, and only fail because of peculiarities
in fundep handling. But fundeps could (and arguably should, to
interact with GADTs and the like) be reworked to behave 'properly'.
It's just that type families already do.
I can't really recall what example I used in the past, but here's one
off the cuff:
module A where
class C a b | a - b where
instance C a a where
data T a where
CT :: C a b = b - T a
module B where
import A
instance C Int Char where
c :: Char
c = case t of { CT x - x }
So, the question is: what should happen here?
We've created a T Int in a context in which C Int Int, so it wraps an
Int. Then we match in a context in which C Int Char. But the fundep
tells us that there can only be one S such that C Int S. So we have
some choices:
1) Disallow the overlapping instance C Int Char, because it is
incompatible with the C Int Int from the other module. This is what
GHC 7 seems to do.
2) Pretend that there may in fact be more than one instance C Int a,
and so we can't infer what a is in the body of c. I think this is what
GHC used to do, but it means that whether a fundep a - b actually
allows us to determine what b is from knowing a is kind of ad-hoc and
inconsistent.
3) Allow c to type check. This is unsound.
1 is, I think, in line with type families. But it rules out the
computation that fundeps + overlapping can do and type families
cannot.
Also, in an unrelated direction: there are conditions on type families
that can allow some overlapping to be permitted. For instance, if you
simply want a closed type function, like, taking the above as an
example:
type family F a :: * where
instance F Int = Char
instance F a = a
Then this is a sufficient condition for overlapping to be permissible.
And it covers a lot of the use cases for overlapping instances, I
think.
-- Dan
___
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
Thanks for the responses. I realized after sending the message that it wasn't clear exactly what I was advocating, which is probably more modest that what people are thinking. Mostly I was hoping the AssociatedTypes wiki page could be updated to reflect that AssociatedTypes can't replace FunctionalDependencies. (After reading the FunctionalDependencies page, I converted a bunch of code over to TypeFamilies, thinking this would be more future-proof, only to realize it couldn't work.) I'm not sure what the process is for updating the wiki, as the page is locked down, but mailing haskell-prime seemed like a reasonable start. I'm absolutely not advocating making overlapping instances (or, worse, overlapping types) part of Haskell', nor under the impression that the committee would ever consider doing so. I'm just pointing out that right now OverlappingInstances are the only way to do recursive programming at the type level, for the specific reasons I outlined. I hope that before FunctionalDependencies or TypeFamilies or any other type-level programming becomes part of Haskell', there is a way to differentiate base and recursive cases *without* overlapping instances. The fact that TypeFamilies made it somewhat far into the process without a way to do recursion and that the limitation is not even documented on the wiki suggests that the Haskell' committee either thinks people don't care or thinks about the question differently. Either way, the point seemed worth noting somewhere. I don't have any great ideas on supporting recursion, so I suggested a not so great idea in my last email that abused the context. Here's another not so great idea that doesn't abuse the context... The point is just that it's possible to support recursion without overlapping instances: Add an annotation like | x /~ y, ... to instances denoting that the instance cannot be selected unless types x and y are known to be different. So the code from my previous message becomes: data HNil = HNil deriving (Show) data HCons h t = h :* t deriving (Show) infixr 2 :* class HLookup k l where type HLookupResult k l hLookup :: k - l - HLookupResult k l instance HLookup k (HCons (k, v) l) where ... type HLookupResult k (HCons (k, v) l) = v hLookup _ (h :* t) = snd h instance (HLookup k l) = HLookup k (HCons h l) | h /~ (k, v) where -- This is how we avoid overlap ^^^ type HLookupResult k (HCons h t) = HLookupResult k t hLookup k (h :* t) = hLookup k t I'm under no illusions that this specific syntax would fly, but possibly some other proposal will allow the equivalent. David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
Re: TypeFamilies vs. FunctionalDependencies type-level recursion
At Sun, 29 May 2011 19:35:15 -0400, Dan Doel wrote: On Sun, May 29, 2011 at 6:45 PM, Ben Millwood hask...@benmachine.co.uk wrote: 1) Disallow the overlapping instance C Int Char, because it is incompatible with the C Int Int from the other module. This is what GHC 7 seems to do. This seems like the only reasonable option given the meaning of functional dependencies. Also, in an unrelated direction: there are conditions on type families that can allow some overlapping to be permitted. For instance, if you simply want a closed type function, like, taking the above as an example: type family F a :: * where instance F Int = Char instance F a = a Something like this would be good. Though you'd need a corresponding value-level mechanism. Is this part of any pending proposal? I don't suppose there's any way to get GHC to accept such code? I only found one cryptic mention of closed synonym families under a speculative ideas list for type functions. David ___ Haskell-prime mailing list Haskell-prime@haskell.org http://www.haskell.org/mailman/listinfo/haskell-prime
