Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unsaturated type families #242

Merged
merged 47 commits into from Dec 4, 2020

Conversation

@kcsongor
Copy link
Contributor

@kcsongor kcsongor commented Jun 16, 2019

The proposal has been accepted; the following discussion is mostly of historic interest.


This is a proposal to allow partial application of type families, as
described in the paper Higher-Order Type-level Programming in Haskell

Rendered

@goldfirere
Copy link
Contributor

@goldfirere goldfirere commented Jun 16, 2019

Hooray! I've been hoping to see this proposal for some time. Unsurprisingly, I think this is a great leap forward. However, I have some quibbles with the details:

  1. As highlighted in Section 3.1, there is an inconsistency around the naming of the arrows. A comment there says (quite rightly) that types of terms will be unmatchable (because we have no matchable functions in terms other than data constructors) and that "the arrow is rendered as -> in terms". I think you mean "in the types of terms" there... but how will that be implemented? It's unclear to me that GHC knows the difference between types of terms and types of types in a way that means it will print arrows consistently.

    Furthermore, I worry with this naming scheme that any future move toward dependent types -- and using ordinary term-level functions in types -- with be hamstrung.

    So might I humbly suggest that we swap the names? Then, -> will be unmatchable and ~> will be matchable. Sadly, this will be a breaking change (but could be easily guarded by the extension), changing the meaning of, e.g., forall (m :: Type -> Type). .... Yet the vast vast majority of arrows in Haskell code are in types of terms, which will continue to be spelled correctly.

  2. It is worth considering a different spelling of the new arrow. Many fonts render ~> too similarly to ->.

  3. The proposal uses ->{m} notation but does not explain it.

  4. Formatting trouble under "Inference".

  5. Why have "Arity of type families"? I would think that type family A :: Type ~> Type and type family B (x :: Type) :: Type would be fully identical. Is there a reason they can't be?

  6. Though I'm responsible for using the word "matchable" in this way, I wonder if we shouldn't rethink. Here's a problem: Suppose I write type family F :: Type -> Type where F Int = Bool. That is rightly rejected. I ask "Why?" You say "You can't match on the argument to F because the argument to F is matchable. You can match only on unmatchable arguments." I say "😫".

  7. The proposal considers interaction with #111: Linear Types: "Happily, multiplicities are only used in types, whereas matchabilities only appear in kinds. As a result, these features are completely orthogonal." However, types and kinds are the same in GHC. How can we tell these apart? I don't think sorting this out will be this easy.

  8. I'm in full support of matchability polymorphism over the subtyping approach in my thesis.

  9. "type inference with the matchability defaulting scheme is incomplete": Very helpful example! I'm not sure you mean "dependency order" there, but I agree that this problem exists, may be soluble, but is likely not worth solving.

  10. We don't need to steal syntax for this (I think): the new operator can always just be imported.

Please don't take these comments as a lack of support for this -- I think it's great. I just want to refine the edges a bit. Thanks for posting.

@RyanGlScott
Copy link
Contributor

@RyanGlScott RyanGlScott commented Jun 17, 2019

I've also been eagerly awaiting this proposal. I apologize in advance for dumping another wall of questions :)

  • I don't have a particular favorite choice of syntax for unmatchable/matchable arrows, but I agree with @goldfirere's point (10) and wonder if we should avoid baking new syntax directly into the parser and instead require users to import the new arrow themselves (perhaps from Data.Arrow).

    This would pose some complications in the implementation, since the fixity of -> is essentially negative infinity due to the fact that it is hard-coded in the parser, and as a consequence, it is impossible to give user-defined type operators the same precedence as ->. This results is oddities like the one observed in this GHC issue, where a ~> b -> c associates as (a ~> b) -> c, not as a ~> (b -> c) like you would intuitively expect.

  • The special ->{m} notation makes me a little nervous, especially since I think that the Linear Haskell prototype is using something similar. (Or perhaps I'm not remembering that correctly).

    Either way, I'm not terribly fond of blessing matchability as the one property of arrows that gets special bracket syntax, as there are other type parameters in (->) that could also be specified (e.g., the RuntimeRep arguments). I think it would be worthwhile to figure out a syntax that lets us specify all of these properties (or a subset of these properties), especially since arrows are only going to be getting even more type parameters in a Linear Haskell future.

  • Speaking of which, what is the full definition of (->) (the matchability polymorphic one) under this proposal? Should we consider having some primitive ARROW type constructor (à la TYPE) now that it has three arguments (the matchability argument and two RuntimeRep arguments)?

  • As far as I can tell, this only proposes to add syntax for A ~> B (i.e., unmatchable visible, non-dependent quantification), and not any of the following (terminology taken from here):

    • forall a ~> B (unmatchable visible, dependent quantification)
    • forall a '. B (unmatchable invisible, dependent quantification)
    • C '=> B (unmatchable invisible, non-dependent quantification)

    Is this intended? I worry that without those, we will run into limitations such as this one.

  • As I observed here, there are potential backwards-compatibility issues with respect to Haskell constructs where the distinction between types and kinds isn't clear. For example, in the following program:

    data T = MkT (Type -> Type)
    type S = MkT Maybe

    If one compiles this program with UnsaturatedTypeFamilies enabled, then according to the specification in this proposal, this will fail to typecheck. This is because Section 3.1 dictates that term-level arrows are assigned to be unmatchable, so MkT (Type -> Type) (a term-level data constructor) is really sugar for MkT (Type ~> Type). However, in the type synonym S, it's not clear whether the type synonym will be used for a type or a kind (as type synonyms can denote both), so the kind of Maybe in type S = MkT Maybe is Type -> Type, not Type ~> Type. Yikes!

    You proposed a more nuanced matchability inference story here which would solve this problem. Should this be mentioned in the proposal?

  • What is the specification regarding definitional equality between partially applied type families? For instance, consider the following two type family definitions:

    type family Id1 x where Id1 x = x
    type family Id2 x where Id2 x = x

    Is Id1 equal to Id2? Can you write type class instances on top of Id1 and Id2? If so, will the instance for Id1 overlap with the instance for Id2?

@Icelandjack
Copy link
Contributor

@Icelandjack Icelandjack commented Jun 17, 2019

I have no technical comments but I take (~>) to mean a polymorphic function, this could lead to confusion. The paper uses the barbed arrow , (->>) would make a good choice

@AntC2
Copy link
Contributor

@AntC2 AntC2 commented Jun 18, 2019

@goldfirere Though I'm responsible for using the word "matchable" in this way, I wonder if we shouldn't rethink. ... "You can't match on the argument to F because the argument to F is matchable. You can match only on unmatchable arguments." I say "tired_face".

Seconded. I'm afraid "(un)matchable" means nothing to me. (Then I have no intuition which flavour of arrow I should be using. Or what the flavour of arrow means if I see it in a signature.) And there's no crisp definition in the proposal -- which there should be, even if there's already definitions in the papers. If we had a definition, perhaps it'd be easier to find a more specific word. The paper section 2.2 says "both injective and generative".

Haskell already uses the word in the sense of 'pattern matching'. And at least one compiler gives you pattern match failure exceptions. So I agree with @goldfirere's intuition that "unmatchable" should give a rejection. But presumably "matchable" here has nothing to do with patterns(?)

The key concept for writing code is saturating the arguments/partial application. For a type family, you must supply the first n arguments to obtain a injective and generative type; for a datatype constructor n is zero.

Seeing as it's in the title of the proposal: "(un)saturated"; or invent a word "(un)injenerative".

Many fonts render ~> too similarly to ->.

Seconded. I often find myself squinting to see whether I'm looking at a tilde or a dash. I am unconvinced we need more than one arrow/decorating the arrow seems to me putting the abstraction in the wrong place, see below.

[proposal] Then equalities of the shape f a ~ g b are only solved by decomposition when f :: k -> j and g :: k -> j.

Equalities using tilde are only solved when the arrow is non-tilde. Seems backwards to me.

[proposal] The proposed change is to distinguish between type constructors and type functions in the kind system.

I don't want to nit-pick over wording, but I often see claims that type functions are type constructors. (For example in the discussion about Row Polymorphism #180 ). It is still confusing the heck out of me. But here you want to distinguish type constructors that are not type functions. Can I call those 'datatype constructors', or is that another blue?

Being a datatype constructor vs a type function is a property of the whole name (which might take several arguments). Then it doesn't seem right to make it a property that falls in between successive arguments (as with differently-flavoured arrows). Could there be something of either of these signatures

k1 ~> k2 -> k3 ~> k4
k1 -> k2 ~> k3 -> k4

If not, why not; and why (apparently) does the proposal allow me to write signatures like that?

(Whichever way round we choose to decorate the arrows.) That seems to me not to show the idea that the first n arguments must be saturated. I'd rather stick with just the one familiar arrow and put some kind of marker at the point we reach saturation:

k1 -> k2 -> k3 | -> k4   -- must supply 3 args to be saturated -- a typical type family
k1 | -> k2 -> k3 -> k4   -- must supply 1 arg to be saturated -- return a higher-kind from a type family
k1 -> k2 -> k3 -> k4     -- no saturation marker, so assume at zero/is a datatype constructor

Or put the marker just after the ->, as you have for the {m} decoration. For a matchability polymorphic TF, use a different marker. (Using a decoration with what looks like a variable name is downright confusing. Could I have k1 ->{m1} k2 ->{m2} k3 -> k4? And do I now have type (kind) variables m1, m2 in scope?) Again I think the required abstraction is to mark n arguments up to a point in the signature.

type family Map (f :: a -> ? b) (xs :: [a]) :: [b] where
  Map _ '[]       = '[]
  Map f (x ': xs) = f x ': Map f xs

Argument f to type function Map can have from zero up to a maximum of 1 argument to obtain a saturated type. (? I've pulled out of thin air/is eminently bikesheddable. It's potentially a user-defined type operator, unlike |; but as such couldn't legitimately appear immediately after ->. I suppose ->? or ?-> (no space) could be a user-defined operator. But we're becoming more relaxed about space-significance #229.)

@AntC2
Copy link
Contributor

@AntC2 AntC2 commented Jun 18, 2019

While I'm on the topic, do we actually need all that business about matchability polymorphism? Couldn't we just say all type families are potentially matchable-polymorphic: in the sense the n arguments is a maximum/you can always supply a type argument whose saturation point is less than n? Then where that happens, type inference/injectivity/generativity can be more eager.)

IOW is there a use case where you'd want to accept Map Id but reject Map Maybe?

@kcsongor
Copy link
Contributor Author

@kcsongor kcsongor commented Jun 19, 2019

Thank you all for taking the time to read the proposal! Let me address some of the questions here, in order. I will defer discussing the syntax for now, but I'm in general agreement with your suggestions @goldfirere.

The proposal uses ->{m} notation but does not explain it.

I've fixed this omission.

Why have "Arity of type families"? I would think that type family A :: Type ~> Type and type family B (x :: Type) :: Type would be fully identical. Is there a reason they can't be?

The arity of a type family still very much matters. Firstly, the generated axioms still have a fixed arity, and they only reduce when fully saturated. In other words, Const Int is perfectly fine as an unsaturated type family application, but there is no corresponding axiom to reduce it.
Related to this, the equational theory doesn't include eta-rules, which means that

type family Id1 (a :: Type) :: Type where
  Id1 x = x

type family Id2 (a :: Type) :: Type where
  Id2 x = Id1 x

type family Id3 :: Type ~> Type where
  Id3 = Id1

here, Id1 ~ Id3 is derivable, but Id1 ~ Id2 is not.

I should add that it would be possible to compute the arity of a type family from the equations, and
not their signature (as is done for terms), which would mean that

type family Id2' :: Type ~> Type where
  Id2' x = Id1 x

could work too. The issue here is with open type families, whose arity would then need to be computed from the declarations which can be in different modules. Or maybe it wouldn't be an issue? The equations are already checked against each other to ensure they don't overlap, so perhaps this check would be relatively straightforward to implement.

The proposal considers interaction with #111: Linear Types: "Happily, multiplicities are only used in types, whereas matchabilities only appear in kinds. As a result, these features are completely orthogonal." However, types and kinds are the same in GHC. How can we tell these apart? I don't think sorting this out will be this easy.

What I meant is that all type arrows are unmatchable, and all kind arrows have omega multiplicity, so there aren't any interesting interactions to consider. The code paths are entirely separate.

"type inference with the matchability defaulting scheme is incomplete": Very helpful example! I'm not sure you mean "dependency order" there, but I agree that this problem exists, may be soluble, but is likely not worth solving.

Here's a sketch of the algorithm:
Consider the constraint a b ~ c Id, with all a, b, c having unsolved matchabilities m_a, m_b and m_c respectively. We can emit an implication constraint which observes that if a and c are matchable, then the equality can be decomposed:
(m_a ~ Matchable, m_c ~ Matchable) => b ~ Id. Every equality constraint between applications would give rise to such implication constraints. Then, we only default the matchabilities that do not appear on the right hand side of implications (here, m_b does, m_b ~ Unmatchable is derivable from the RHS). Then keep doing this until all matchabilities are either derived or defaulted.

@RyanGlScott:

As far as I can tell, this only proposes to add syntax for A ~> B (i.e., unmatchable visible, non-dependent quantification), and not any of the following (terminology taken from here):

Good point, I agree these should be included too.

What is the specification regarding definitional equality between partially applied type families?
Is Id1 equal to Id2? Can you write type class instances on top of Id1 and Id2? If so, will the instance for Id1 overlap with the instance for Id2?

See above. But to answer, they are not equal, though nor are they apart. Type class instances for type families is not part of this proposal. I would like to have that feature, probably as a separate proposal once this one is settled. The trouble is that for instance matching, we really want a decidable apartness relation (otherwise instance selection would be undecidable even between instances that don't have contexts). For this, we would ideally like to determine that Id1 and Id2 are apart. But doing that would not be forward compatible with extensions to the type system such as eta. The tension could be resolved by introducing a new role that has restricted computation rules compared to the existing nominal one, which would then be used in instance selection. Anyway, this is outside of the scope of the current proposal.

@AntC2:

Equalities using tilde are only solved when the arrow is non-tilde. Seems backwards to me.

This is a really good point. I have not considered the relation, and the potential for confusion here.

Could there be something of either of these signatures [...] If not, why not; and why (apparently) does the proposal allow me to write signatures like that?

In Haskell, every kind is inhabited, and you can write a type family with either of those kinds. Granted, this type family will have no instances, but I don't see that as a reason for disallowing the kind.

That seems to me not to show the idea that the first n arguments must be saturated. I'd rather stick with just the one familiar arrow and put some kind of marker at the point we reach saturation:

This is an interesting idea, however, I think it wouldn't be very compositional, as it would essentially mean that the whole kind is now one big unit, and a lot of additional bookkeping is required to keep things together. How would you abstract over such a thing?

Using a decoration with what looks like a variable name is downright confusing. Could I have k1 ->{m1} k2 ->{m2} k3 -> k4? And do I now have type (kind) variables m1, m2 in scope?

Indeed, you can! They are truly variables, and we get m1 and m2 in scope. That said, I'm happy to change the syntax if we find something that looks better.

While I'm on the topic, do we actually need all that business about matchability polymorphism?

I think we do. Having higher-order type functions and staying with first-order unification poses a number of challenges, and I believe that such a first-class solution is the most predictable, even if there is some mental overhead.


The outstanding question seems to be what to do with the arrow. Make -> the unmatchable one, and introduce a different arrow for matchables? What would be a good migration path for that?

@RyanGlScott
Copy link
Contributor

@RyanGlScott RyanGlScott commented Jun 19, 2019

Type class instances for type families is not part of this proposal.

Gotcha. It might be worth mentioning in the proposal that attempting to define a class instance (or type family instance) on top of an unsaturated type family should be an error, then.

I might seem fixated on this point, but that's only because the singletons library currently defines type class instances for defunctionalization symbols, so the inability to define instances for unsaturated type families might pose a problem if singletons abandons defunctionalization in favor of UnsaturatedTypeFamilies. Of course, the needs of singletons shouldn't drive the specification of this proposal, but given that your paper draws inspiration from singletons' notation, I couldn't help but feel a tad bit disappointed that UnsaturatedTypeFamilies couldn't be a drop-in replacement for defunctionalization in it current state :)

To be clear, though, I agree that this is a challenging problem that is best left for a different proposal.

@jberryman
Copy link

@jberryman jberryman commented Jun 19, 2019

Is there a commonly used library that would make use of this proposal? If so would love to see an example of what Joe User would see in the docs, what from this proposal they'd need to understand to be productive, etc.

As a library writer I'd be happy to be subjected to the complexity in this proposal in order to express the API I want. As a user I don't want to learn about anything here (the ideal is I never have to consider the issue being addressed here, right?; the language just becomes simpler).

If the proposal means common libs go the way of undefined where no one is quite sure what the type means anymore that's a Drawback that should be discussed I think.

Thanks for your work on this!

@simonpj
Copy link

@simonpj simonpj commented Jun 19, 2019

I like the proposal in general.

Syntax is the hardest bit.!

  • In "Specification" the proposal badly needs clear statement of the syntactic changes, by way of a BNF delta. You say you've fixed the lack of explanation of ->{m} but I don't see such an explanation.

  • It's hard to avoid the connection with linearity polymorphism. Both decorate the arrow, in a possibly-polymorphic way. But, currently, I think linear arrows will appear only in the types of term-level functions, while matchabilty arrows will appear only in the kinds of type-level functions.

  • I think linearity polymorphism is moving in the direciton of t1 # lin -> t2 meaning an arrow from t1 to t2 decorated with linerity lin. It would be odd not to use a related syntax for both. You propose t1 ->{m} t2; but if we use that, we should arguably use it (or some related form) for linearity polymorphism too.

  • Linearity polymorphism has operators that connect linearity, so you can have say

    f :: forall l m. (Int # l -> Int) -> (Int # m -> Int) -> Int #(l && m) -> Int
    

    (I'm sure I have the details wrong.) Do you need any functions of type Matchability -> Matchabilty -> Matchability or are the annotations always a constant or a variable?

@simonpj
Copy link

@simonpj simonpj commented Jun 19, 2019

type inference with the matchability defaulting scheme is incomplete

That suggest that you have a "matchability defaulting scheme" in mind. What is it?

I think this issue arises only when kind-checking type signatures. So in your example we have

nested :: a b ~ c Id => b Bool

I think you are suggesting

  • Kind-check the signature
  • Simplify the constraints that arise
  • Default any unconstraint matchability variables to Matchable
  • Based on that, further simplify the constraints
  • And quantify over unconstrained kind variables

The worry is that defaulting them all at once might be wrong. Perhaps defaulting would fix another. Or vice versa.

I don't understand your suggestion about implication constraints I'm afraid.

@AntC2
Copy link
Contributor

@AntC2 AntC2 commented Jun 19, 2019

Could there be something of either of these signatures [...]

In Haskell, every kind is inhabited, and you can write a type family with either of those kinds. Granted, this type family will have no instances, ...

Thanks @kcsongor for all the replies. Let me see if I can work what this kind would mean. I need to put the parens into the signatures, I think:

k1 ~> (k2 -> (k3 ~> k4))          -- was k1 ~> k2 -> k3 ~> k4

takes first argument a type family; second argument a datatype constructor; third argument a type family(?)

k1 -> (k2 ~> (k3 -> k4))          -- was k1 -> k2 ~> k3 -> k4

takes first argument a datatype constructor; second argument a type family; third argument a datatype constructor(?) Does that mean that if we already have the first argument, type inference can take advantage of it being generative?

So the decoration on the arrow tells us about the argument to its left?

  1. I'm still feeling that putting the decoration on the arrow is the wrong place: it applies for the argument.
  2. ref @simonpj's point on the {m} decoration, the matchability also applies for the argument to the left, so that should appear left of the arrow -- which conveniently coincides with the position of the linearity decoration.

The outstanding question seems to be what to do with the arrow. Make -> the unmatchable one ... ?

I'm going to repeat: I see no need for different flavour of arrows. If we need to decorate the arrow anyway for matchability polymorphism (and I'll put that to the left)

k1 {U} -> k2 {M} -> k3 {U} -> k4   -- upper case so not a tyvar

Now to my eye that could be decorating the argument, just as much as decorating the arrow.

Yes that's verbose; but I take it the defaulting rules will mean you seldom actually write it in code. Readers of displayed matchability-marked signatures will see it.

Except I'm not happy with U, M because they stand for (Un)Matchable and that means nothing to me. (Un)Saturated -- as in 'the argument to the left can be Unsaturated/must be Saturated to make it injective&generative'?

The { } braces indicate a required explicit type (kind) argument if they surround a tyvar; and there I'm putting a type (which therefore doesn't get explicitly applied). Is that going to upset anybody's aesthetics? Then we could borrow from linear types and put #; or put the explicit type application in the signature

k1 # U -> k2 # S -> k3 # U -> k4 

k1 @U -> k2 @S -> k3 @U -> k4 

@AntC2
Copy link
Contributor

@AntC2 AntC2 commented Jun 19, 2019

While I'm on the topic, do we actually need all that business about matchability polymorphism?

I think we do. Having higher-order type functions and staying with first-order unification poses a number of challenges, and I believe that such a first-class solution is the most predictable, even if there is some mental overhead.

I should have been clearer: I'm not trying to interfere with the implementation under the hood. I'm wondering why we need to expose it so "tiresomely" to the programmer:

When supplying type arguments to matchability-polymorphic functions such as ...
the user needs to provide either a concrete matchability or a wildcard before supplying the instantiation for f, as in qux @_ @Id. This is tiresome, because m can always be inferred from the kind of f, ...

  1. OK, so just go ahead and infer it, and don't bother me with putting useless @_. And if that means the polymorphism decoration can't be { }, then all the better. Use # _ -- in coordination with the linearity stuff, of course.
  2. I see no use case for a "concrete matchability". Again: why would you want to accept Map Id but reject Map Maybe?

At term level we don't say: here you must supply an expression with a function, you're not allowed to put a data constructor.

@isovector
Copy link
Contributor

@isovector isovector commented Jun 19, 2019

@jberryman I'm particularly excited about this proposal as a library writer. It makes using the higher-kinded data pattern feasible. It would allow us to write this:

type family HKD f a where
  HKD Identity a = a
  HKD f a = f a

data Person (f :: Type ~> Type) = Person
  { pName :: f String
  , pAge :: f Int
  } deriving (Eq, Ord, Show)

The unmatchable arrow on f lets GHC derive the instances, which it currently cannot do. Instead we are resigned to one of the two following solutions today, both of which are terrible:

deriving instance Eq (Person Identity)
deriving instance Ord (Person Identity)
deriving instance Show (Person Identity)

deriving instance Eq (Person Maybe)
deriving instance Ord (Person Maybe)
deriving instance Show (Person Maybe)
-- and also for every other type at which you instantiate this

-- O(distinct types used) number of instances

or

deriving instance Eq (Person Identity)
deriving instance Ord (Person Identity)
deriving instance Show (Person Identity)

deriving instance (Eq (f String), Eq (f Int)) => Eq (Person f)
deriving instance (Ord (f String), Ord (f Int)) => Ord (Person f)
deriving instance (Show (f String), Show (f Int)) => Show (Person f)

-- O(number of fields) size of instance constraints

OK, but when would such a thing be useful, you might wonder? Both beam and ecstasy both aggressively use this pattern. Beam rejects the HKD-ness --- requiring a bunch of boilerplate to pattern match out your Identitys --- while ecstasy requires the instances above.

@monoidal
Copy link
Contributor

@monoidal monoidal commented Jun 19, 2019

Does this proposal affect type synonyms? Given type T a = a -> a we can give T the same type as if we had type instance T a = a -> a. Currently in ghci there's a hack to make :kind T work (even though T is not a legal type in Haskell) and we could get rid of it.

@jberryman
Copy link

@jberryman jberryman commented Jun 20, 2019

@isovector You mean that HKD becomes unnecessary under this proposal, right? Because you can now write ... :: Person Id, where we have something like type family Id a where Id a = a.

Or do you mean we still have pName :: HKD f String ... etc? And the arrow would need to be matchability polymorphic right?

I don't totally follow how this allows deriving instances in the way we'd want but agree that looks like it changes the game for this pattern! So I guess what I'm looking for is an accurate view of how e.g. beam's API might change under this proposal (just one or two types and functions would be fine).

I'm also curious if you think parameterizing an HKD like Person by a traditional open type family would actually be useful (I don't have a good intuition for this pattern yet). I got the sense some of the challenge/complications in this proposal are due to non-injectivity of type synonym families (I may be totally wrong), and so I wonder if a simpler solution could satisfy 80% of use cases, say.

@Ericson2314
Copy link
Contributor

@Ericson2314 Ericson2314 commented Jun 21, 2019

@AntC2

I'm still feeling that putting the decoration on the arrow is the wrong place: it applies for the argument.

That and a few other of your comments leads me to think you think "matchability" applies to the function parameter. It doesn't; it really is about the function itself. @goldfirere in his these for example allows

case x :: a -> Either a b of
  Left -> ...
  Right -> ...

and

case x :: Type -> Type of
  Maybe -> ...
  List -> ...
  _ -> ...

This proposal doesn't go as far as the thesis, but the idea is that type constructor equality and variant equality are decidable in the same way.

[@goldfirere mentioned regretting some of the terminology, I don't quite know whether/how that applies to the above.]

@AntC2
Copy link
Contributor

@AntC2 AntC2 commented Jun 21, 2019

Thanks @Ericson2314 then all I can say is that the current state of the proposal is making a terrible job of explaining what's going on. Typically the text from these proposals goes forward to the Users Guide. (And with other proposals I've had cause to get the Users Guide dramatically rewritten, precisely because the Guide followed the proposal text, not what the extension actually does.) Then I suggest this proposal is not ready. I don't expect (nor do I expect the audience of the Users Guide) to have to read @goldfirere's thesis to be able to use this feature -- not even to read the paper.

I'm all for making the type language more consistent with the term language. Then explain this: Haskell doesn't at term level distinguish between functions that take (partially applied) functions as arguments vs functions that take (partially applied) data constructors as arguments. Indeed Haskell at term level doesn't distinguish whether anything is partially applied or saturated. It just has to be the right type. Then where's this claim coming from that "The aim of this proposal is to bring the type language closer to the term language ..."?

I get it that type functions are not like term-level functions, because the types (kinds) of type functions are not generative nor injective (usually). Then it seems to me that "bring[ing] the type language closer to the term language" is impossible, and the claim is bogus. And this proposal should just say it's to support partially-applying type functions (a good thing), and stop making overblown promises.

Specifically

The proposed change is to distinguish between type constructors and type functions in the kind system.
This new version of Map can now only be applied to type families, but not type constructors, ...

How is that not "appl[ying] to the function parameter."? (parameter as type constructor vs as type function)

... it really is about the function itself.

My first line of enquiry was to suggest it's about the function as a whole; and @kcsongor corrected that by saying a function-as-a-whole might have a mix of ->, ~> arrows in its kind. Now you seem to be contradicting that: "... applies to the function parameter. It doesn't;". What wording/explanation is going into the Users Guide?

This proposal doesn't go as far as the thesis, ...

Then pointing me to the thesis is no sort of explanation of this proposal. And I don't understand your example quoted from the thesis (those are (promoted) type constructors, so generative/injective, so can appear unsaturated OK, so have nothing to do with the case); and it doesn't appear in the proposal; so it just seems a distraction.

[ mentioned regretting some of the terminology, ...]

The specific term to be possibly regretted is "matchability", on grounds it seems to be counter-intuitive to what can be matched. "allowed to appear unsaturated" might be a more felicitous term, but hardly trips off the tongue.

" [doesn't ] appl[y] to the function parameter. ...; it really is about the function itself." isn't helping my intuition either.

@Ericson2314
Copy link
Contributor

@Ericson2314 Ericson2314 commented Jun 21, 2019

@AntC2

The simpler way to combine the type and term languages is just to remove this axiom at all levels. And that's what Agda and Idris do! But people complain about type inference being bad and those languages, and we absolutely don't want to create a regression! The alternative is differentiating our fs and gs on both levels so we a) unify the languages b) keep the axiom over it's original domain b) don't regress.

It's certainly possible. Finding the commonality between two fixed things and faithfully recreating them at the library, rather than language, level is an ancient FP trick. That's all that's being done here.

How is that not "appl[ying] to the function parameter."? (parameter as type constructor vs as type function)

Map is a higher order type family. The matchability-polymorphic function is not Map itself (the outer arrow in the kind) but it's parameter (the inner arrow in the kind).

My first line of enquiry was to suggest it's about the function as a whole; and @kcsongor corrected that by saying a function-as-a-whole might have a mix of ->, ~> arrows in its kind. Now you seem to be contradicting that: "... applies to the function parameter. It doesn't;".

I agree with @kcsongor. I think the confusion was that there merely being a mix of arrows in the kind doesn't say which one, why.

"allowed to appear unsaturated" might be a more felicitous term, but hardly trips off the tongue.

But with this proposal everything is allowed to be unsaturated. You might not get fan automatic equality reasoning from GHC when you do something really fancy, but you certainly won't be directly forced to add more arguments.

@monoidal
Copy link
Contributor

@monoidal monoidal commented Jun 25, 2019

Is there an interaction with promotion? For example, can I declare data A where MkA :: X ~> A and use MkA on the type level?

Will there be an equivalent of -fprint-explicit-runtime-reps (that is, not showing Matchability variables by default and zapping them to Matchable)?

Is there interaction with top-level kind signatures?

@isovector
Copy link
Contributor

@isovector isovector commented Aug 11, 2019

I'm really excited about this proposal. @kcsongor is there anything in the way of submitting this to the committee?

@kcsongor
Copy link
Contributor Author

@kcsongor kcsongor commented Aug 13, 2019

@isovector I will update the proposal in light of the comments here, but most likely that will be after ICFP (which is next week).

@tydeu
Copy link

@tydeu tydeu commented Sep 15, 2019

I am a bit confused as to why this proposal is so complex given the fact that we can already simulate unsaturated type families in current GHC.

For instance, we can implement the Map example in the proposal like so:

infixl 9 :$:
data f :$: a

type family Map (f :: k) (xs :: [a]) :: [b] where
    Map _ '[]       = '[]
    Map f (x ': xs) = BR (f :$: x) ': Map f xs

type family Id a where
  Id a = a

-- Type-level beta reduction
type family BR (a :: k1) :: k2

data Map'
type instance BR Map' = Map'
type instance BR (Map' :$: f) = (Map' :$: f)
type instance BR (Map' :$: f :$: a) = Map f a

data Id'
type instance BR Id' = Id'
type instance BR (Id' :$: a) = Id a 

type instance BR Maybe = Maybe
type instance BR (Maybe :$: a) = Maybe a

type MaybeMap' = Map' :$: Maybe
type DoMaybeMap = BR (MaybeMap' :$: '[Int, Bool])
-- DoMaybeMap == '[Maybe Int, Maybe Bool]

type DoIdMap = BR (Map' :$: Id' :$: '[Int, Bool])
-- DoIdMap == '[Int, Bool]

Thus, it seems like we could alternatively implement unsaturated types (and type-level lambdas in general) by doing something like the following:

  • Desugaring type-level application f a to BR (f :$: a)
  • Reducing completely unsaturated type family names (and possibly type synonyms) to some unique type (i.e. like the prime types in the above example)
  • Creating a magic type family BR that maps to the given type family (or type synonym) when given fully saturated application of its name. Otherwise it is the identity function.

My point with all this is that this proposal seems to be adding a lot of complexity to the type system when that might not be necessary. This seems especially true since the end goal is currently essentially achievable, just not in a particularly pretty way.

@LeanderK
Copy link

@LeanderK LeanderK commented Oct 2, 2019

this proposal introduces the matchability polymorphism through the mixfix syntax: ->{m}. But, as a side effect, it doesn't allow one to use the mixfix syntax for other stuff, does it?

Example:
type a ~~>{cat} b = cat a b

@nomeata
Copy link
Contributor

@nomeata nomeata commented Dec 4, 2020

Don’t worry Simon, I don’t expect I’d propose reject it in its current form, but I do want to apply the limited due dilligence I can.

Or maybe I have misunderstood what the alternative you are proposing is.

I am not proposing anyhing, merely asking for clarification on this sentence in the proposal

Instead of matchability polymorphism, a subsumption relationship could be considered between the two arrows. This approach has been fully formalised by Richard Eisenberg in his thesis. The main drawback of that approach is that inference would suffer compared to the scheme outlined above. Matchability polymorphism also fits more cleanly into the existing constraint solver mechanism.

and I am wondering if we have two viable designs here, with different pros and cons, that we can weigh against each other, or if the subsumption-based design is practically unfeasiable, and there is no choice to consider.

Copy link
Contributor Author

@kcsongor kcsongor left a comment

Thanks for the comments/questions/suggestions @gridaphobe!
I tried to address all of them and updated the text where I thought it made sense.

(sorry for the spam, I found out halfway through that I can batch up my responses)

proposals/0000-unsaturated-type-families.rst Outdated Show resolved Hide resolved
proposals/0000-unsaturated-type-families.rst Show resolved Hide resolved
proposals/0000-unsaturated-type-families.rst Show resolved Hide resolved
proposals/0000-unsaturated-type-families.rst Outdated Show resolved Hide resolved
gridaphobe
Copy link
Contributor

gridaphobe commented on c86672a Dec 4, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We don't yet know at this point that term-level functions are unmatchable, or why. Maybe it would make sense to move the "Term-level functions" section to the top here and deal with it up front? Explain (1) why we even assign matchabilities to term-level functions, and (2) why they're always unmatchable. I think the answers are

  1. The type-level arrow and kind-level arrow are the same thing, so we kind of have to assign a matchability to term-level functions. Also, we're slowly moving toward a dependent future, at which point we will care about the matchability of term-level functions.

  2. I'm actually not entirely sure of this, but I would reason by analogy from the rules around type families. We say that type families are unmatchable when they bind their arguments, presumably because this means they have the ability to compute on their arguments. In contrast, tycons and datacons are just carriers of their arguments. In particular, a type family that does not bind its arguments and whose RHS is matchable is also matchable, e.g.

      -- inferred: Type -> @M Type
      type MyMaybe :: Type -> Type
      type family MyMaybe where
        MyMaybe = Maybe
    

    Functions are made to do computation, so it makes sense that they would also default to unmatchable. But, just like a type family could be defined directly in terms of a tycon, a function could be defined directly in terms of a datacon. So, would it be similarly safe to infer matchability of functions?

      -- inferred: a -> @M Maybe a
      myJust :: a -> Maybe a
      myJust = Just
    

    This would cause problems for the term-level story, if nothing else, as GHC would not currently eta-expand myJust. But is there a deeper reason we could not (or should not) do this?

kcsongor
Copy link
Contributor

kcsongor commented on c86672a Dec 4, 2020

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I like that suggestion -- I've moved "term-level functions" before "data constructors", it reads better now in my opinion.

  1. That's exactly the reason. I updated the text to reflect this point.
  2. There is no deeper reason we couldn't do this, in fact I think that the eta-expansion could produce a matchability-polymorphic wrapper instead of unmatchable, much like how it produces a multiplicity-polymorphic wrapper. That way Dependent Haskell would have a lot more ergonomic story around matchabilities.
    (It's something I've been meaning to try in the implementation, but so far I've been holding off putting more work into it until the proposal's fate has been decided)

Co-authored-by: Eric Seidel <github@eric.seidel.io>
@gridaphobe
Copy link
Contributor

@gridaphobe gridaphobe commented Dec 4, 2020

Thanks @kcsongor! I think the overview and examples are much easier to follow now.

I have one last question around backwards compatibility. The proposal is pitched as parameterized in the specific defaulting rules, but it's not entirely clear to me how painful it would be to change the defaulting rules from the initial specification. How likely is it that a change to the defaulting rules would break programs that do not enable UnsaturatedTypeFamilies? I realize this could vary heavily by the specific rule, but I'm trying to get a sense for how delicate the current balance is. Also, are there any current defaulting rules that would break existing code? (I thought I saw one marked as such in my first read, but now I can't find it.)

I'm bringing this up because while the plan seems to be to accept this as an experimental extension, it does affect all haskell code (though hopefully nobody will notice), just like LinearTypes. So I just want to be careful that we don't get ourselves into a bind later.

@kcsongor
Copy link
Contributor Author

@kcsongor kcsongor commented Dec 4, 2020

The way the current rules are designed is that it should be possible to turn on the extension, and have most existing programs compile. Any subsequent change to the rules (and in particular migrating to a version that aims to be more future compatible than backwards compatible) will mean that some programs will then require annotations that didn't before (but some programs will no longer require annotations that do now). Given that the current design is backwards compatible, making that change then is going to be no more painful than starting with that design now, the only difference is when we will have to endure that pain.

For programs that do not enable UnsaturatedTypeFamilies, alternative designs would more likely cause breakage. I'm not sure yet how much of that can be mitigated. The most delicate part of the proposal is the handling of higher-order arguments to type constructors and type families. Changing these from defaulting to matchable will have the largest effect.

An option (which is written in the proposal) is that the switch will happen when Dependent Haskell lands, with the understanding that it's a breaking change. The defaulting rules are so delicate because of the way type families work (namely they treat all arguments are relevant when a kind signature is given, and can do typecase). If Dependent Haskell retires type families in favour of "plain old functions", then we can infer way more polymorphism and have the best of both worlds.

With all of that said, if the proposal is accepted, I expect that the rules might converge to a more satisfactory status quo before merging the implementation, depending on #378 among other things.

@goldfirere
Copy link
Contributor

@goldfirere goldfirere commented Dec 4, 2020

After hearing no firm objections from the committee, I declare this proposal accepted. However, several members of the committee (including myself, along with @kcsongor evidently) are unsure about the defaulting rules. In addition, this proposal describes a wholly new feature for Haskell (for programming languages generally, actually). It will thus be accepted experimentally, meaning that we accept that the final implementation may differ from this proposal on the finer points. These changes would be made in consultation with the GHC developers and will, in the end, be posted as an amendment to this accepted proposal. It is our expectation that the light of experience may lead us to continue tinkering here even after release.

Specifically, there are two points in this proposal still unresolved:

  • The syntax. Should we go ahead with the proposal as written, or use modifiers in line with #370?
  • The defaulting rules.

I will now merge the proposal, adding some text declaring parts of the proposal still not-quite-settled.

Thanks for the informative debate everyone. I'm excited to see this get into GHC!

@kcsongor
Copy link
Contributor Author

@kcsongor kcsongor commented Dec 4, 2020

Thanks for shepherding the proposal @goldfirere and thanks again everyone for the valuable contributions!

@gridaphobe
Copy link
Contributor

@gridaphobe gridaphobe commented Dec 4, 2020

Thanks @kcsongor, that was a very helpful clarification! And thanks for submitting the proposal, I'm also very excited to see this in GHC!

@goldfirere goldfirere merged commit b83b493 into ghc-proposals:master Dec 4, 2020
@goldfirere goldfirere changed the title Unsaturated type families (under review) Unsaturated type families Dec 4, 2020
@cgibbard
Copy link
Contributor

@cgibbard cgibbard commented Dec 4, 2020

Hey, I know this was already merged and all, but can someone please give a mathematically coherent definition of "matchable" and for the unary sense of "generative" with the quantifiers put in explicitly? I have no idea how to read these definitions such that anything makes any sense.

It sounds like "f and g are generative" means "either f and g have disjoint ranges or are equal", though without quantifiers it's hard to tell, but then immediately "f is generative" gets used, and despite hanging a lampshade on the abuse of a binary relation as a unary one, it's unclear what's actually meant by such a condition. "f and f are generative"? Well, that's going to be trivially the case, since f ~ f, so probably isn't what is meant. "For all g, f and g are generative"? "There exists g such that f and g are generative"? "f and some unmentioned specific function F are generative"? Something else?

Since I can't tell what unary generative means, I then don't know what matchable is supposed to mean.

The rules later in the paper seem to declare by fiat that type constructor applications give matchable arrows, and type family applications give unmatchable arrows, but I'm not certain how to connect that back to the definitions given before.

@kcsongor
Copy link
Contributor Author

@kcsongor kcsongor commented Dec 5, 2020

@cgibbard Admittedly, giving a formal notion of "matchability" is not an aim of the
proposal, and I appreciate that the wording might have caused confusion. So I hope this
clears some of it up.

Generativity is a relation between two functions (f g : A -> B)

generative f g = forall (x y : A). f x ~ g y -> f ~ g

Your reading is the correct one: "either f and g have disjoint ranges or are
equal" (see Footnote 1). This relation is reflexive and symmetric, but not transitive (see
Footnote 2) when considering all type functions. What we're looking for is a
subset of type functions where generativity is an equivalence relation, and in
particular an equivalence class of this subrelation. Then we will call members of
this set "generative".

There are many ways of constructing such sets, and the idea in this proposal is
to identify a syntactic way of generating one such set, namely by considering
type constructors, for any pair of which the generativity relation holds.

So, type constructors are "generative", and again, this means that the set of
type constructors is an equivalence class; in other words, any two type constructors
either have disjoint ranges or are equal. (My guess is that the name here comes
from the fact that type constructors "generate" new types disjoint from every existing
type, but @goldfirere might be in a better position to answer this, as I believe the name
comes from him).

The unary notion of "matchability" is obtained in a similar way by considering
the subset of generative functions that are injective as well (all type
constructors have this property, but it is useful to treat the two properties
separately), and in particular picking one such equivalence class, the set of
type constructors.

In general the relation is undecidable, but this syntactic approximation is (cheaply) decidable.
Importantly, when two type functions have a matchable kind, the generative rule is derivable
for them in the system, but for two unmatchable functions, the negation is not derivable,
so we can't decide that two functions are "different" when they are unmatchable.

To summarise, the aim of matchability is to characterise a set of injective type
functions whose range is pairwise disjoint, and we use a syntactic approximation to
pick one suitable set, which happens to line up with GHC's existing type inference
mechanism.


Footnote 1:
The ~ sign in the discussion above refers to GHC's propositional equality, and
it leaves some room for some future extensions. For example, we might want to
also allow eta-expanded type constructors in this relation when we have type
lambdas.

Footnote 2:

To see why it's not transitive, consider

type family F a where
  F Int = Maybe Bool
  F a = Int

type family G where
  G Int = [Bool]
  G a = Bool

then generative F G holds (as they have disjoint ranges) and generative G Maybe holds too,
but not generative F Maybe.

@kcsongor kcsongor deleted the unsaturated-type-families branch Dec 5, 2020
@kindaro
Copy link

@kindaro kindaro commented Jan 23, 2021

What is the place to build GHC with this feature from now? I used to build from Csongor's fork — is it still the place, or is there now a branch in the main GHC repository? And how can I follow the continued work on this extension?

@kindaro
Copy link

@kindaro kindaro commented Feb 3, 2021

Ping @goldfirere @kcsongor, see previous comment please!

@kcsongor
Copy link
Contributor Author

@kcsongor kcsongor commented Feb 3, 2021

@kindaro As of now, that is still the most recent buildable version. I've been working on rebasing my patch on top of the refactored flattener/rewriter in HEAD, and also updating the fork to reflect the final version of the proposal. Unfortunately, there's still an infinite loop lurking somewhere I haven't yet managed to catch, but it's getting there.

@kindaro
Copy link

@kindaro kindaro commented Feb 3, 2021

Thanks Csongor. I have already tried things with this patch and it worked great. I hope it gets merged to official GHC soon!

@JakobBruenker
Copy link
Contributor

@JakobBruenker JakobBruenker commented Aug 17, 2021

I had a case today where I had a type family like

type F :: k -> Type -> Type
type family F a env where
  F (B b) env = G a env
  F a     env = H a env

and needed a constraint F a ~ H a, which is not possible since that would be an unsaturated application. I was able to work around this with some effort, but I'm wondering, are unsaturated applications like this inside equality constraints possible with this proposal, and, given, say, a ~ Int, would GHC be able to determine that F a ~ H a? Or can it only reduce type family applications once all arguments are supplied?

@kcsongor
Copy link
Contributor Author

@kcsongor kcsongor commented Aug 17, 2021

Yes, unsaturated applications are supported within equality constraints too, but type families are only reduced once all arguments are supplied.

@JakobBruenker
Copy link
Contributor

@JakobBruenker JakobBruenker commented Aug 17, 2021

That makes sense, thank you

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
Linked issues

Successfully merging this pull request may close these issues.

None yet