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 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 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

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.