June 2011 - Haskell-prime

TypeFamilies vs. FunctionalDependencies & type-level recursion
by David Mazieres 05 Jul '11

05 Jul '11

I'm not sure if these extensions are still under discussion or if the topic is dead (wiki pages 5 years old). However, the Haskell' wiki page for FunctionalDependencies suggests AssociatedTypes is a more promising approach, yet the AssociatedTypes page misses a major Con compared to FunctionalDependencies that I think should be there. 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). As an example, consider the following simple (key, value) lookup function that operates at the type level (inspired by HList): {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE OverlappingInstances #-} {-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE UndecidableInstances #-} data HNil = HNil deriving (Show) data HCons h t = h :* t deriving (Show) infixr 2 :* data A = A deriving (Show) data B = B deriving (Show) data C = C deriving (Show) abc :: HCons (A, Int) (HCons (B, Int) (HCons (C, Int) HNil)) abc = (A, 1) :* (B, 2) :* (C, 3) :* HNil class HLookup k l v | k l -> v where hLookup :: k -> l -> v instance HLookup k (HCons (k, v) l) v where hLookup _ (h :* t) = snd h instance (HLookup k l v) => HLookup k (HCons h l) v where hLookup k (h :* t) = hLookup k t b :: Int b = hLookup B abc -- Returns 2 The key to hLookup is that OverlappingInstances selects the most specific match, thereby breaking the recursion when the requested key type matches the key of the pair at the head of the list. By contrast, TypeFamilies cannot permit a function such as hLookup. One may try something along the lines of: 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) where type HLookupResult k (HCons h t) = HLookupResult k t hLookup k (h :* t) = hLookup k t 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. 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 ... Of course, I have no idea how the compiler could know such constraints are sufficient to avoid overlapping types. I suspect figuring it out would be hard given that instance matching happens before context verification and that the overlapping errors must happen at instance matching time. My bigger point is that if the Haskell' committee ever considers adopting one of these proposals or one intended to supersede them, I hope there is a way to do recursive type-level programming. A likely corollary is the need for a mechanism to avoid instance overlap between recursive and base cases by asserting type inequality in the recursive case. David

12 38

Proposal: fix "simple pattern binding" and "declaration group"
by dm-list-haskell-prime＠scs.stanford.edu 01 Jul '11

01 Jul '11

The Haskell 2010 report contains ambiguous and sometimes contradictory definitions of the terms "simple pattern binding" and "declaration group". The confusion is compounded by the phrasing of the monomorphism restriction, which is carried over from the Haskell98 report in which a different definition of declaration group required a more complicated description of the monomorphism restriction. A recent thread on the haskell cafe mailing list summarizes the problem: http://www.haskell.org/pipermail/haskell-cafe/2011-June/093488.html To resolve this confusion, I propose applying the following changes to the Haskell 2010 report for the next revision of the language: In section "4.4.3.2 Pattern bindings", replace: - A pattern binding binds variables to values. A simple pattern - binding has form p = e. The pattern p is matched “lazily” as - an irrefutable pattern, as if there were an implicit ~ in - front of it. See the translation in Section 3.12. With the following: A pattern binding binds variables to values. A /simple/ pattern binding is one in which the pattern consists of a single variable, yielding a declaration of the form /var/ /rhs/. Recall from section 3.17 that such a pattern is always irrefutable. In section 4.5.1, replace this text: - A binding b1 depends on a binding b2 in the same list of - declarations if either - - 1. b1 contains a free identifier that has no type signature - and is bound by b2, or with the following: A binding b1 depends on a binding b2 in the same list of declarations if either 1. b1 contains a free identifier v, v is bound by b2, and the list of declarations does not contain a type signature for v; or Add the following text to the end of section 4.5.1: For example, the following two bindings form a single declaration group, as each contains a free identifier bound by the other and, despite the presence of expression type-signatures, the declaration list contains no type signatures: (x, y) = (z :: Int, 1 :: Int) -- binds y, has z free (z, t) = (2 :: Int, y :: Int) -- binds z, has y free Conversely, the following two bindings constitute two different declaration groups. Even though f and g contain each other as free identifiers, the declaration list contains a type signature for f, so g does not depend on f. f :: (Eq a) => (a, a) -> (Bool, a) f = \(x, y) -> (x == y, snd (g (x, y))) g pair = (fst (f pair), snd pair) Note that if b is a function binding or simple pattern binding and b is accompanied by a type signature, then b always constitutes a /singleton/ declaration group, regardless of what free identifiers it contains. (If b is a non-simple pattern binding, it may bind multiple variables simultaneously.) Finally, change Rule 1 of the monomorphism restriction in section 4.5.5, by replacing the following text: - We say that a given declaration group is unrestricted if and - only if: - - (a): every variable in the group is bound by a function - binding or a simple pattern binding (Section 4.4.3.2), - and - - (b): an explicit type signature is given for every variable in - the group that is bound by simple pattern binding. with the following: We say that a given declaration group is unrestricted if and only if: (a): every variable in the group is bound by a function binding, or (b): the group consists of exactly one binding, the binding is a simple pattern binding of some variable v, and the binding's declaration list contains an explicit type signature for v. If there is agreement on these changes or something along these lines, I can create a ticket and/or wiki page. I propose the name SimplePatternBinding for the change. David

3 5

Re: TypeFamilies vs. etc - TTypeable
by Anthony Clayden 28 Jun '11

28 Jun '11

Thank you Oleg >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. > ........ So this is essentially the approach discussed in the HList paper, translated to a Type Family context. Totally brilliant, and almost impenetrable. If I understand what's going on (big IF), I'm wondering a few things: - You've used type-level NAT to encode the type. What if two different types get encoded as the same NAT? In your MonadState example you've encoded StateT as FOUR ::: NAT, and W as FIVE. What if there's some other module (in a distant import) that also uses FOUR? In general, how do we co-ordinate the encoding of types to avoid duplicates? - Special instances: you say for MonadState' "add more if needed". But can we really do that? The default instance has constructor MState hard coded in the result of function MState'. - Groundedness issues (per Section 9 of the HList paper, 'Reification ...' subsection. The instances of TYPEOF require the type constructor to be grounded; and TYPEOF recurses to reify all the constructor's type arguments. Does this mean all types and arguments have to be fully grounded? Is this really gaining anything over the Type-indexed rows approach you discuss in the HList paper - that is, using instances instance TypeEq x x HTrue instance (b ~ HFalse) => TypeEq x y b -- (using ~ instead of TypeCast) except that it's avoiding fundeps and overlapping instances? That is: is the TYPEOF approach to type equality going to suffer the same issues discussed at the start of section 9 'By chance or by design'? I'm imagining a Haskell' with type functions and a restrained sort of instance overlap: type instance TypeEqF x x = HTrue type instance TypeEqF x y | x /~ y = HFalse (Which is roughly what last month's Haskell-prime discussion talked about, and SPJ picked up on at the start of this TypeFamilies thread.) AntC

2 2

Re: TypeFamilies vs. etc - restrined instance overlap type inference
by Anthony Clayden 26 Jun '11

26 Jun '11

Hi all some more, Continuing the idea of a restrained form of instance overlap for type functions ... Type inference I don't expect to be totally decidable, so that may torpedo the idea altogether. I do expect it to be more coherent than GHC's current handling of overlap with fundeps. What's impressive is how much of a 'cottage industry' has grown up using overlaps. Do we really want to throw all that away? SPJ summarises that the idea is that: > ... 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). In my earlier post I proposed how to validate instances so that they don't overlap (although the instance heads might do), by using type inequality restraints. In an ancient mail list discussion of similar ideas [haskell-prime February 2006 'overlapping instances and constraints'] when type families were first mooted, SPJ commented: "Concerning [a suggested approach] it involves *search* which the current mechanism does not. Presumably you have in mind that the type system should "commit" only when there is only one remaining instance declaration that can fit. You need to be very careful not to prune off search branches prematurely, because in a traditional HM type checker you don't know what all the type are completely. And you need to take functional dependencies into account during the search (but not irrevocably). I have not implemented this in GHC. I don't know anyone who has. I don't even know anyone who has specified it. All good stuff to debate. [...] In general, I think that type-system proposals are much easier to evaluate when accompanied with formal type rules. It's not just a macho thing -- it really helps in debugging the dark corners. " Inference for instances without restraints proceeds as usual. Instances with type inequality restraints are validated not to overlap those without, so if there's an instance that fits, we can apply it confidently. What we do need is rules for how type inference gathers evidence of a type inequality from the type environment. Once we've inferred that evidence, we can 'fit' to the instance head and apply the RHS of the type function (or apply the type Class). Evidence of type inequality: Base case: T t1 t2 ... tn /~ U u1 u2 ... um, where T, U type constructors and T /= U n, m >= 0 Derived case: T t1 t2 ... tn /~ T u1 u2 ... un, where T type constructor And ti /~ ui for some i (I suspect this is far as GHC tries currently to discriminate overlaps, based on the groundedness experiments discussed in the HList paper section 9. I think it's possible to get a bit further ...) also derived: t t1 t2 ... tn /~ t u1 u2 ... un, where t is a type term AND ti /~ ui (t can be type term except a type function) and: T t1 t2 ... tn /~ t u1 u2 ... un, if ti /~ ui, where T type constructor (again t can be any type term except a type function note that matching type args is from the right-hand end, because t might turn out to be of the form (tt uu1 uu2 ...) essentially: whatever t resolves to, the overall types must be unequal) as well: T t1 t2 ... tn /~ t u1 u2 ... um, where T type constructor And m > n (t any type term except a type function, if m > n then t's arity is more than T's, so they can't be the same.) Algebra: Type inequality is symmetric: t /~ u ==> u /~ t transitive across equality: t /~ u, u ~ v ==> t /~ v My (highly hand-wavy) understanding from the 'outside-in' papers of how type inference proceeds is that the possible instances 'compete' to apply until one fits. (If there would be several that might fit, it's 'first come first served'. So it's essential under GHC's current forms of type families that overlapping instances are confluent.) With type inequality restraints we keep to that rule: inference must not apply an instance until the type environment provides evidence of the inequality. AntC

1 0

Re: TypeFamilies vs. etc - restrained instance overlap
by Anthony Clayden 26 Jun '11

26 Jun '11

Hi all THE TOPIC: [from the original post] >TypeFamilies vs. FunctionalDependencies & type-level recursion >David Mazieres dm-list-haskell-prime at scs.stanford.edu >Sun May 29 20:59:44 CEST 2011 >... 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", ... >Of course, I have no idea how the compiler could know such constraints >are sufficient to avoid overlapping types. ... I think I do have an idea - see below. More important, how does type inference proceed without the dreaded *search* and potentially premature commit to an instance? I've also some ideas on that. (But this post will already be long enough, see separately for type inference.) THE WHAT: [SPJ responded to the OP] >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. > .... (example that needed overlapping instances, so rejected for type families) > But you can with fundeps > class Eq a b c | a b -> c > instance Eq k k True > instance Eq j k False As other posters pointed out, this form isn't quite right, and the form that works is more cumbersome and obscure. The thread then veered away into how fundeps could be improved, mostly resulting in the rules becoming even harder to understand (at least for me). SPJ mused: >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). THE HOW: I'd like to tackle this from another approach: what would it need to extend type families with a restrained form of instances? (Because, like SPJ "A big reason I like type families better is simply that I can understand them.") I prefer the following style: type family Eq a b :: * -- not closed type instance Eq k k = TTrue type instance Eq j k | j /~ k = TFalse -- effectively this makes the type family closed (Variations of this idea have appeared and reappeared at various times [at least since "A Theory of Overloading" Stuckey & Sulzmann, ICFP 2002, section 8.2, using disequalities in CHR's]. I'm keenly aware that the Haskell-prime process is only supposed to consider already-implemented extensions, so I'm trying to draw in as much pre-existing work as possible.) (The pattern-guard style of syntax seems natural, but I'll leave others to debate the lexicals ;-) Other examples: instance (Monad m) => MonadState s (StateT s m) where ... instance (Monad (t m), MonadTrans t, MonadState s m) => MonadState s (t m) | (t m) /~ (StateT s m) where .. type instance IsFunction (a -> b) = TTrue type instance IsFunction a | a /~ (_ -> _) = TFalse -- using _ as 'don't care' type var THE WHY: Advantages: A1: Each instance 'stands alone' (so they don't have to be defined in the same place). This approach avoids one difficulty SPJ points out about sequence of equations: >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. A2: The instances don't overlap, although the instance heads do. So ... A3: Introducing a new instance (perhaps imported from an ostensibly unrelated module) does not 'silently' change behaviour. (One of the long-standing complaints about overlaps.) That is: if the new instance overlaps, we get a compile fail. A4: And we can validate instances for overlap 'there and then' as the compiler encounters each instance. That is, how Hugs behaves, whereas GHC currently defers validating overlap until it encounters a use-site where it can't figure out which instance to choose. GHC's behaviour was a source of confusion even in the thread that followed SPJ's post, because instances appeared to compile clean, but in fact couldn't be used. THE HOW (part 1 - validating instances): Instance validation uses mechanisms already in GHC for the limited forms of overlap it supports in Type Families: V0: The terms each side of the /~ must be of the same Kind (same rule as for type equalities). V1: Upon encountering each instance, compare it one by one with all other instances in scope. V2: If the heads don't overlap, we're OK. V3: If they do overlap, form the mgu for the overlap. V4: Substitute the mgu into the RHS of the instances, if they're confluent we're OK. (Up to this point is existing GHC behaviour.) V5: If they do overlap but aren't confluent, and neither has a disequality restraint, reject. V6: If <none of the above>, substitute the mgu into the disequality(s) for the instance(s). At least one must lead to a contradiction. Example from GHC's documentation for type families: > type instance G (a, Int) = [a] > type instance G (Char, b) = [b] -- ILLEGAL overlap on G (Char, Int) > type instance G (Bool, b) | b /~ Int = [b] > -- legal, because substituting the mgu for the overlap yields > -- G (Bool, Int) | Int /~ Int -- at validation step V6 THE HOW (part 2 - type inference): see the next episode. ... Ends AntC

1 0

TypeFamilies vs. FunctionalDependencies & type-level recursion
by oleg＠okmij.org 17 Jun '11

17 Jun '11

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 HList does NOT depend on that invalid behavior. The bug is relatively recent (introduced around 2006); HList worked in 2004.

5 10

Re: TypeFamilies vs. FunctionalDependencies & type-level recursion
by Dan Doel 16 Jun '11

16 Jun '11

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-prime(a)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

5 12