Partial type family application

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

Partial type family application

mniip
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)
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

mniip
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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

David Feuer
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 <[hidden email]> 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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

Richard Eisenberg-4
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 <[hidden email]> 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 <[hidden email]> 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.

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

Jan Stolarek
In reply to this post by mniip
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.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

mniip
In reply to this post by Richard Eisenberg-4
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
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

Richard Eisenberg-4

> On Apr 26, 2017, at 8:39 PM, mniip <[hidden email]> 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

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

oleg-30
In reply to this post by mniip

If the goal is to write higher-order type families, we can do that
already -- and were able to do for a long time.

For example, please see
        http://okmij.org/ftp/Haskell/TTypeable/TTypeable.hs
that was written in 2012 for
        http://okmij.org/ftp/Haskell/typeEQ.html

It shows the type-level function that checks for a membership in a
type-level using the equality function supplied by a user as the first
argument. Incidentally, here is the definition


type instance Member f x NIL = HFalse
type instance Member f x (h :/ t) =
  ORELSE (Apply f (x,h)) (CLOS AC_Member (f,x,t))

It was written before the modern syntax for type-level lists and
booleans.

This is an example of the general technique of defunctionalization.


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

mniip
In reply to this post by Richard Eisenberg-4
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?
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: Partial type family application

mniip
In reply to this post by mniip
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
_______________________________________________
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.