Partial type family application
So I've been thinking of a type system extension: partial type family application. If we look at the type system used by modern GHC, in it, type family application is very distinct from constructor/constraint application: it is somewhat opaque in the sense that a type family must always appear fully applied. As such, it doesn't make sense to talk about a type family's kind, if we have: type family Id (a :: *) :: * where Id x = x then saying that 'Id :: * -> *' would be wrong, because Id cannot be used interchangeably with things that are truly of kind * -> *, such as Maybe or []. The reason for the "fully applied" restriction is that if we allowed partially applied type functions, then their equality would be undecidable. Still, I think, in a lot of cases we could benefit from partially applied type functions, even without extensional equality. Writing type level list folds, filters, zips, you name it. As stated above, we can't add the proposition 'Id :: * -> *' to our type system, so, what if, instead, we added a different kind of arrow kind for type families? I like the look of (~>), so 'Id :: * ~> *'. (~>) :: * -> * -> * This rule of inference, similar to the usual, would supersede all the type family kinding rules: f :: k ~> l, x :: k ------------------- f x :: l As such, the juxtaposition operator would very clearly have two different "kinds": (k -> l) --> k --> l and (k ~> l) --> k --> l, and there is no N-ary "type family application" operator. In order for the type checker to not fall apart, we need to have at least intesional (structural) equality on (~>), which we can have because it is decidable. We could then write stuff like type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where Foldr f z '[] = z Foldr f z (x ': xs) = f x (Foldr f z xs)
Oops, got cut off :S We could then write stuff like type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where Foldr f z '[] = z Foldr f z (x ': xs) = f x (Foldr f z xs) type family Flip (f :: k ~> l ~> m) (x :: l) (y :: k) :: m where Flip f x y = f y x -- Lift a type constructor into a type family type family Apply (con :: k -> l) (x :: k) :: l where Apply con x = con x type family (.) (f :: l ~> m) (g :: k ~> l) (x :: k) :: l where (.) f g x = f (g x) stuff :: Foldr (Flip (Apply . Apply (,))) () '[Int, String, Char] stuff = ((((), 'x'), "moo"), 3) This idea is very fresh, and I certainly haven't explored all the aspects, so I would welcome constructive (and intuitionistic) criticism regarding both usefulness and mathematical soundness of this. --mniip
The arrow distinction is something I've speculated about, but I don't see how to handle nullary families and families with implicit kind arguments. These aren't necessarily written with arrows at all. type family F :: * type instance F = Char type family G :: k type instance G = Int type instance G = 'True On Wed, Apr 26, 2017 at 8:29 AM, mniip <14@mniip.com> wrote:
Oops, got cut off :S
We could then write stuff like
type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where Foldr f z '[] = z Foldr f z (x ': xs) = f x (Foldr f z xs)
type family Flip (f :: k ~> l ~> m) (x :: l) (y :: k) :: m where Flip f x y = f y x
-- Lift a type constructor into a type family type family Apply (con :: k -> l) (x :: k) :: l where Apply con x = con x
type family (.) (f :: l ~> m) (g :: k ~> l) (x :: k) :: l where (.) f g x = f (g x)
stuff :: Foldr (Flip (Apply . Apply (,))) () '[Int, String, Char] stuff = ((((), 'x'), "moo"), 3)
This idea is very fresh, and I certainly haven't explored all the aspects, so I would welcome constructive (and intuitionistic) criticism regarding both usefulness and mathematical soundness of this.
--mniip _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
Yes, I believe you’re describing the Right Answer to this problem. I’ve hinted at this in my “Promoting functions to type families paper” (http://cs.brynmawr.edu/~rae/papers/2014/promotion/promotion.pdf) -- see Sections 4.3.1 and 7.1. It’s unfortunate that this clean idea is buried in all the other stuff in that paper. I’ve also mused on this approach in my thesis (http://cs.brynmawr.edu/~rae/papers/2016/thesis/eisenberg-thesis.pdf); see Section 4.2.4 (which seems readable independent of the rest of the thesis). The good news here is that this idea should be realizable independent from Dependent Haskell. It just needs someone to work out the details, propose, get community acceptance, and implement. But, from a theory point of view, I’m confident you’re describing the right direction to take all this in. Richard
On Apr 26, 2017, at 10:08 AM, David Feuer <david.feuer@gmail.com> wrote:
The arrow distinction is something I've speculated about, but I don't see how to handle nullary families and families with implicit kind arguments. These aren't necessarily written with arrows at all.
type family F :: * type instance F = Char
type family G :: k type instance G = Int type instance G = 'True
On Wed, Apr 26, 2017 at 8:29 AM, mniip <14@mniip.com> wrote:
Oops, got cut off :S
We could then write stuff like
type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where Foldr f z '[] = z Foldr f z (x ': xs) = f x (Foldr f z xs)
type family Flip (f :: k ~> l ~> m) (x :: l) (y :: k) :: m where Flip f x y = f y x
-- Lift a type constructor into a type family type family Apply (con :: k -> l) (x :: k) :: l where Apply con x = con x
type family (.) (f :: l ~> m) (g :: k ~> l) (x :: k) :: l where (.) f g x = f (g x)
stuff :: Foldr (Flip (Apply . Apply (,))) () '[Int, String, Char] stuff = ((((), 'x'), "moo"), 3)
This idea is very fresh, and I certainly haven't explored all the aspects, so I would welcome constructive (and intuitionistic) criticism regarding both usefulness and mathematical soundness of this.
--mniip _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
On Wed, Apr 26, 2017 at 10:58:10AM -0400, Richard Eisenberg wrote:
The good news here is that this idea should be realizable independent from Dependent Haskell. It just needs someone to work out the details, propose, get community acceptance, and implement. But, from a theory point of view, I’m confident you’re describing the right direction to take all this in.
I'm reading your thesis, and in it you propose to make all -> arrows unmatchable, and all constructors automagically get '-> arrows. Naturally, if we implement just this type extension, then it'd make sense to leave the -> arrow as is and introduce an ~> unmatchable arrow. However this makes transition to fully dependent arrows even more awkward. On the other hand we would have to pull the implicit '-> constructor arrows into this proposal, which makes it not so independent from dependent types, so still awkward. What do you think should be done? --mniip
On Apr 26, 2017, at 8:39 PM, mniip <14@mniip.com> wrote:
I'm reading your thesis, and in it you propose to make all -> arrows unmatchable, and all constructors automagically get '-> arrows.
Yes, that's what it says.
Naturally, if we implement just this type extension, then it'd make sense to leave the -> arrow as is and introduce an ~> unmatchable arrow. However this makes transition to fully dependent arrows even more awkward.
But what *is* the (->) arrow? In a type describing a term, (->) describes an unmatchable function. In a kind describing a type, it describes a matchable function. And this is the tension. -XTypeInType means that types and kinds are the same, so this discrepancy is even stranger. It doesn't really bite, quite, but I very much think that any work in this direction should aim to have (->) be unequivocally unmatchable (because unmatchable functions are the vastly common case, taking both terms and types into account). As far as I can tell, a matchable -> occurs in Haskell today in kind signatures and the type signature of a GADT-style data constructor. These spots are easy to discern syntactically, so it's not hard to keep this legacy behavior in a brave new world with first-class matchable and unmatchable arrows. I would see phasing these out at some point -- it also wouldn't be hard to write a tool to automatically change current usage of arrows to the new one. But perhaps the community wouldn't want this (that is, phase out current usage), and that's fine too. Also: I have no strong opinions at all about the spelling of the new arrow. Using '-> had some nice similarity with other uses of ', but ~> is a notation I've also long considered.
On the other hand we would have to pull the implicit '-> constructor arrows into this proposal, which makes it not so independent from dependent types, so still awkward.
Yes, if we say that -> is always unmatchable, then the implicit treatment of -> in certain syntactic situations would have to become part of this proposal, making it a little harder to implement. And if we consider this proposal in the absence of dependent types, your choice of notation might make more sense. (To be clear, "your choice" is, as I understand: -> describes an unmatchable function in terms, -> describes a matchable function in types, and ~> describes an unmatchable function in types.) So I see how the possibility of dependent types colors this proposal.
What do you think should be done?
I still maintain the opinion I present in my thesis, that -> should always be unmatchable and some new symbol (I propose '->, but have no strong opinion) should always be matchable. We would have support for legacy uses of -> in kinds, perhaps disabled with -XCurriedTypeFamilies (just because -XUnsaturatedTypeFamilies isn't quite as tasty). That said, I can see the virtue of the opposing viewpoint and would happily debate this on a ghc-proposal. Richard
On Wed, Apr 26, 2017 at 09:20:34PM -0400, Richard Eisenberg wrote:
But what *is* the (->) arrow? In a type describing a term, (->) describes an unmatchable function. In a kind describing a type, it describes a matchable function. And this is the tension. -XTypeInType means that types and kinds are the same, so this discrepancy is even stranger. It doesn't really bite, quite, but I very much think that any work in this direction should aim to have (->) be unequivocally unmatchable (because unmatchable functions are the vastly common case, taking both terms and types into account).
After some more reading, I think I understand what you mean here.
As far as I can tell, a matchable -> occurs in Haskell today in kind signatures and the type signature of a GADT-style data constructor.
Why is a GADT constructor's arrow matchable? A GADT constructor is indistinguishable from a term function in that you can't pattern-match partially applied constructors.
These spots are easy to discern syntactically, so it's not hard to keep this legacy behavior in a brave new world with first-class matchable and unmatchable arrows. I would see phasing these out at some point -- it also wouldn't be hard to write a tool to automatically change current usage of arrows to the new one. But perhaps the community wouldn't want this (that is, phase out current usage), and that's fine too.
I could see that very easily being an issue, yes. Perhaps, if we consider unmatchable arrows as a supertype of matchable arrows, then we could secretly assign matchable arrows in the appropriate places even if an unmatchable arrow was written (why would anyone want an explicitly unmatchable arrow?) and not display them in type signatures until appropriate extensions are enabled. That would be backwards compatible with all current code, and the only place you'd need to use the new arrow would be a higher order type family.
Also: I have no strong opinions at all about the spelling of the new arrow. Using '-> had some nice similarity with other uses of ', but ~> is a notation I've also long considered.
I don't either, and I came up with ~> in a few seconds. Honestly I don't know what a good candidate for it would be. '-> throws me off because it looks more like \hookrightarrow.
and would happily debate this on a ghc-proposal.
On Wed, Apr 26, 2017 at 10:58:10AM -0400, Richard Eisenberg wrote:
The good news here is that this idea should be realizable independent from Dependent Haskell. It just needs someone to work out the details, propose, get community acceptance, and implement. But, from a theory point of view, I’m confident you’re describing the right direction to take all this in.
Are you suggesting that this idea is worthy of a GHC proposal?
mniip, you might want to take a look at a paper Richard Eisenberg and I wrote together in 2014: Eisenberg, R. A., and Stolarek, J.: Promoting Functions to Type Families in Haskell, ACM SIGPLAN Notices 49(12):95-106 (originally published at: Haskell Symposium 2014, Göteborg, Sweden) Janek Dnia środa, 26 kwietnia 2017, mniip napisał:
Oops, got cut off :S
We could then write stuff like
type family Foldr (f :: k ~> l ~> l) (z :: l) (xs :: [k]) :: l where Foldr f z '[] = z Foldr f z (x ': xs) = f x (Foldr f z xs)
type family Flip (f :: k ~> l ~> m) (x :: l) (y :: k) :: m where Flip f x y = f y x
-- Lift a type constructor into a type family type family Apply (con :: k -> l) (x :: k) :: l where Apply con x = con x
type family (.) (f :: l ~> m) (g :: k ~> l) (x :: k) :: l where (.) f g x = f (g x)
stuff :: Foldr (Flip (Apply . Apply (,))) () '[Int, String, Char] stuff = ((((), 'x'), "moo"), 3)
This idea is very fresh, and I certainly haven't explored all the aspects, so I would welcome constructive (and intuitionistic) criticism regarding both usefulness and mathematical soundness of this.
--mniip _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
--- Politechnika Łódzka Lodz University of Technology Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata. Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie. This email contains information intended solely for the use of the individual to whom it is addressed. If you are not the intended recipient or if you have received this message in error, please notify the sender and delete it from your system.
For everyone who didn't notice, the original post was incorporated into this proposal: https://github.com/ghc-proposals/ghc-proposals/pull/52 which attracted less community attention than I hoped it would. Please check it out! On Wed, Apr 26, 2017 at 03:29:32PM +0300, mniip wrote:
This idea is very fresh, and I certainly haven't explored all the aspects, so I would welcome constructive (and intuitionistic) criticism regarding both usefulness and mathematical soundness of this.
--mniip
participants (4)
-
David Feuer -
Jan Stolarek -
mniip -
Richard Eisenberg