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

Add Dependent Haskell quantifiers (including the new "foreach") #102

Open
wants to merge 11 commits into
base: master
from

Conversation

Projects
None yet
@goldfirere
Contributor

goldfirere commented Jan 6, 2018

This proposal reserves syntax for all the quantifiers of Dependent Haskell, along with introducing the -XDependentTypes extension and allowing the new quantifiers to be used in very limited contexts. This proposal does not actually add dependent types.

Rendered

goldfirere added a commit to goldfirere/ghc-proposals that referenced this pull request Jan 6, 2018

@nomeata

This comment has been minimized.

Contributor

nomeata commented Jan 6, 2018

It seems that some aspects of -Wcompat are enabled only when -XDependentTypes, but some compat warnings are introduced even without the extension enabled. Intentional?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 6, 2018

Yes, that was intentional. But even reading it now, I'm not sure it's the best design. The question is about whether, say, data Proxy :: forall k. k -> Type should be accepted in the distant future. That forall really should be a pi. What makes pi a keyword, though? If it's -XDependentTypes, do we want to require someone using kind polymorphism (but not other dependent types) to turn on the extension? Do we just add pi to -XPolyKinds? I don't know. The proposal takes the conservative approach of allowing the Proxy declaration if -XDependentTypes isn't turned on.

@simonpj

This comment has been minimized.

Contributor

simonpj commented Jan 8, 2018

Here, a "kind" is one that can be syntactically recognized as such, by appearing to the right of a :: in a type

This looks highly dubious to me. Proposal #103 is all about trying to avoid such artificial syntactic distinctions. Eg what about a visible kind argument -- is that "syntactically recognised as a kind"?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 8, 2018

According to the proposal, a visible kind argument is not "syntactically recognized as a kind", and I'm not changing that stance. However, you're right that this distinction smells bad. I don't know a better solution, though.

Right now, we use -> to mean two different things: sometimes, it's matchable and sometimes, it's unmatchable. In Dependent Haskell, -> uniquely means unmatchable, and '-> (subject to bikeshedding, if anyone cares to) uniquely means matchable. (Type inference includes a sub-typing relationship between these for convenience. See chapter 6 of my thesis if you dare.)

The problem is that we want to introduce the '-> syntax to allow for backward compatibility later. We also ideally would like to encourage authors to use the new syntax where it should be used: in kinds. This proposal includes a clumsy heuristic (but, I wager, an effective one) for doing so. We could omit this part of the proposal (specifically, point 4 under Semantics:) without great harm.

Do you see a better way to do this?

@Saagar-A

This comment has been minimized.

Saagar-A commented Jan 9, 2018

Bikeshedding: I don't like where the ' is located in the matchable versions of the dependent quantifiers. To me, it makes more sense for it to be associated with the -> or .. Looking something like this:

forall a '->  
forall a '.  
pi a '->  
pi a '.  

This way there is a symmetry between a -> b : forall x -> b and a '-> b : forall x '-> b. Also, this style is future consistent if Haskell were to add dependent linear quantification a ⊸ b : pi x ⊸ b.

Also, using unmatchable arrows in GADT-style data constructors (and only in GADT-style data constructors) should not be a warning or an error. It is clear from context that matchable arrows are meant.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 10, 2018

@Saagar-A Yes, I too noticed the lack of parallel between '-> and 'pi x ->. The one problem with your suggested syntax is that the tick will be confused with a prime. For example, what would forall a'. mean? Is that binding the variable a' (a-prime)? Or is it binding a in a matchable forall? Presumably we would use whitespace to tell the difference, which would work fine, in practice. At this point, I still prefer my syntax, but I'll list your suggestion as an alternative.

@Ericson2314

This comment has been minimized.

Ericson2314 commented Jan 10, 2018

@goldfirere I like that alternative; I'd straight-up allow ' in infix operators across the board to enshrine this without another whitespace hack.

@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Jan 23, 2018

I also prefer the alternative syntax for the matchable dependent quantifiers.

@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Jan 24, 2018

The proposal mentions:

  1. With -XDependentTypes, the matchable arrow becomes required in kind signatures.
  2. With -XDependentTypes, matchable arrows and relevant quantification becomes allowed (but optional) in the kind signatures of a data type.

One thing that I'm unclear on is whether or not the kind signature on a data type declaration requires a matchable arrow. The proposal says:

As described above in the part introducing matchability data constructor arguments are matchable (as are type constructor arguments). Thus, they should be able to use the matchable arrow '->.

This seems weaker than the later statement:

The matchable arrow '-> is required (with -XDependentTypes) in kinds

More concretely, my question is whether or not this will be allowed when -XDependentTypes is on:

data Foo :: Bool -> Type where
  FooC :: Foo 'True

Is the matchable arrow required here or not? Personally, I would like to see stricter, rather than looser, requirements here. In fact, I'd really prefer that pi be required, instead of merely suggested, in data type kind signatures when -XDependentTypes is on. After all, -XDependentHaskell already carries with it the matchable kind signature requirement, so full compatibility with code written without the extension is already out the window. As someone who frequently reads other people's code, I find it easier to understand when people provide as many type signatures and kind signatures as possible. More stringent requirements would may make things a little more difficult for authors, but they would benefit readers by making data type kind signatures more reflective of the actual kind.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Jan 26, 2018

I've updated the proposal with @andrewthad's suggestion about matchability, which I don't fully agree with. Type and data constructor types are so common, and matchability is so esoteric, that I don't want to burden everyone with requiring the matchability annotations. That said, I would support an optional warning that would encourage the pedantic among us to put in the matchability marks.

@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Jan 26, 2018

I like the idea of a -Wpedantic-matchability flag. +1 from me on that.

tebello-thejane and others added some commits Jan 27, 2018

Unmatchable pi quantifiers shouldn't have ticks.
I suppose this is a typo.
Merge pull request #2 from tebello-thejane/patch-2
Unmatchable pi quantifiers shouldn't have ticks.
@glaebhoerl

This comment has been minimized.

glaebhoerl commented Feb 4, 2018

(🚲 warning)

The pi keyword seems awfully jargony to me. Is there no better keyword (or syntax) we could potentially use here?

Consider the connections one has to be able to make to derive from "pi" its intended meaning:

  1. "pi" stands for the greek letter π
  2. Uppercase Π is used in math to denote products
  3. Because they are conceptually products over the inhabitants of the input type, type theory uses Π as one of its notations for dependent functions
  4. Ah, so it's a dependent function

Compare this to forall:

  1. forall a. a -> a means "for all types a, a function from a to a". It reads right off.

(I know that I, personally, was pretty mystified when I first heard about "pi types" many years ago. What the heck does the circumference of a circle have to do with types?)

Given that Haskell probably has more mainstream penetration than all dependently typed languages combined, it seems likely that -XDependentTypes is going to be most peoples' first introduction to dependently typed programming, and we can't really expect them to be already familiar with all of the relevant background.

@cartazio

This comment has been minimized.

cartazio commented Feb 4, 2018

@int-index

This comment has been minimized.

Contributor

int-index commented Feb 4, 2018

Interesting concern raised by @glaebhoerl. My personal favorite to go with forall would be foreach. It makes sense that forall is parametric (we have the same behavior for all instantiations), whereas foreach is not (we may pattern match and define an individual behavior for each instantiation).

@glaebhoerl

This comment has been minimized.

glaebhoerl commented Feb 4, 2018

I had that thought as well, but thought the distinction between "forall" and "foreach" might be too subtle and therefore also surprising. But if other people don't hate it, it seems like a decent alternative to me.

As another possibility, is there any grammatical obstacle to simply leaving off the keyword (or, to preserve symmetry, we could claim that it's Ɛ) and requiring parentheses, for the usual dependent function syntax?

E.g.

-- parametric
forall (n :: Nat) -> Vec n -> Vec n

-- dependent
(n :: Nat) -> Vec n -> Vec n 

Hmm... I just had this GHCi session:

$ ghci
GHCi, version 8.0.2: http://www.haskell.org/ghc/  :? for help
Prelude> :set -XDataKinds -XPolyKinds
Prelude> data Nat = Z | S Nat
Prelude> data Vec (n :: Nat) = Vec
Prelude> let foo :: (n :: Nat) -> Vec n -> Vec n; foo = undefined

<interactive>:5:12: error:
     Expected a type, but n has kind Nat
     In the type signature:
        foo :: (n :: Nat) -> Vec n -> Vec n

Prelude> let bar :: (a :: *) -> Maybe a -> Maybe a; bar a = id
Prelude> 

So that might be a no-go. It's... strange that this syntax is already accepted?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Feb 4, 2018

The syntax that @glaebhoerl suggests directly above is taken, unfortunately. For example, I can say id :: (a :: Type) -> a, where :: Type is a kind signature. Note that this is a different meaning than pi!

@glaebhoerl thanks for the bikeshedding: I had never considered anything but pi for the new keyword, but you make a compelling argument that pi is quite hard to motivate if you're not a type theorist. I have to say that I really like foreach. It's nicely parallel to forall, and the meaning is just about right. (And, @cartazio, I hadn't thought about pi = 3.14. That would indeed be a problem.) It will be hard to retrain my fingers at this point, but I'll update the proposal (and title of the ticket).

@goldfirere goldfirere changed the title from Add "pi" syntax, along with syntax for other Dependent Haskell quantifiers to Add Dependent Haskell quantifiers (including the new "foreach") Feb 4, 2018

@andrewthad

This comment has been minimized.

Contributor

andrewthad commented Feb 4, 2018

My preference would be pi instead of foreach. I'm not worried about the name conflict with the mathematical constant since people could just use another name for it in code where they need it. Ultimately, the committee will have to pick decide what name is used, but I just wanted to make sure that there's one voice out there in favor of pi.

The mediocre argument I can offer is an argument from precedent. Haskell tends to pick mathematical names for abstractions rather than intuitive names. Every now and then, I see a discussion on the libraries list about why Functor wasn't named Mappable (and similar concerns around Applicative, Monad, Monoid, Semigroup, etc.). The advantages are that it makes it easier to discuss the thing or to learn about what it means outside the context of haskell.

@RyanGlScott

This comment has been minimized.

Contributor

RyanGlScott commented Apr 1, 2018

Apologies for asking questions about proposals that have already been submitted to the committee, but a handful of questions about this feature popped into my mind recently.

  1. Currently, there's a forall-or-nothing rule (see #103) which states that any type signature headed by an explicit forall must explicitly quantify all of its type variables. How will the forall-or-nothing rule evolve with the addition of these new quantifiers? Will type signatures like these:

    f :: forall a -> b -> Either a b
    g :: foreach a. a -> b -> Either a b
    h :: foreach a -> b -> Either a b

    be rejected for not explicitly quantifying b?

  2. How does this feature interact with TypeApplications? Currently, one can use TypeApplications on type variables that were bound with the forall. quantifier. Will this property extend to all of the other quantifiers introduced in this proposal? A subset of them?

  3. GHC currently has a warning when you quantify a type variable with forall. but don't use it anywhere, such as in:

    foo :: forall a. Int
    foo = 42
    warning: [-Wunused-foralls]
        Unused quantified type variable ‘a’
        In the type ‘forall a. Int’
    

    Do you think that a similar warning is warranted when you use a dependent quantifier but don't use it anywhere? My understanding is that this:

    bar :: foreach a -> Int
    bar x = x

    could just have well been given the type signature Int -> Int, since a is not actually used in a dependent fashion anywhere in the type signature (save for its binding site). Note that saying a is "unused" would be inaccurate here, since removing a would change the type, but perhaps GHC could warn that foreach a could be changed to Int.

    A similar question applies to visible foralls.

  4. Will GHC throw an error message if I try to forall-quantify something relevantly? In other words, can GHC infer the relevance of each variable and check that the user-provided relevance matches up with the inferred relevance?

    Conversely, if I use foreach irrelevantly, will GHC warn me?

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Apr 2, 2018

Great questions! Thanks for asking.

  1. I think all those should be rejected as not obeying the forall-or-nothing rule.

  2. TypeApplications can be used to bind a forall- or foreach-quantified invisible variable. That is, it will work with both forall a. and foreach a. (and their matchable forms). It will thus be seen more as an invisibility-override than a type-application marker.

  3. Yes, we should warn for dependently-quantified variables never used in a dependent way. But I'm unsold as to where this warning should go in GHC's warning hierarchy. Naming parameters is useful documentation, and other languages sometimes require users to do this, even when the names are redundant. (I'm looking at you, Java interfaces.) Even where these aren't required, they are allowed (C/C++ header files, all those dependently typed languages).

  4. A forall-quantified variable used relevantly is a type error, pure and simple. A foreach-quantified variable not used relevantly should induce a warning, yes. This latter case can't happen, though, under this proposal, as foreach is very restricted. I don't think either of these cases can happen with this proposal, though.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Apr 2, 2018

I went to update the proposal with my answers above, but there seems to be no need. I don't think any of these cases can actually arise with the restrictions in this proposal and more properly belong in some future proposal that introduces dependent types properly.

@Centril

This comment has been minimized.

Centril commented Apr 8, 2018

After some reflection, my view on pi, foreach and forall is that the two latter ones are too close together to not cause confusion between dependent and parametric modes. That foreach and forall have a subtle distinction is in other words not a good thing.

The word pi however, while being quite jargon-y, is clearly distinct from forall, and is therefore quite easy to search for on the internet. For someone who is trying to learn more advanced concepts in Haskell, it should therefore be relatively easy to search for "Haskell pi" and one of the first results will then (most likely) be a (hopefully good) explanation of this. By using pi we also give the reader easy access to a host of learning materials that will also pop up in the search results.

As an experiment / anecdata, try to search for "Haskell foreach" on google;

While pi might give a Haskell some ridicule or flack from people who joke about burritos and such, I think it is superior to foreach for findability and learnability. But I will agree that it is bad for marketing purposes.

As an alternative I'd like to propose: pifor, which may be too weird, but well; consider it =)

@rrnewton

This comment has been minimized.

rrnewton commented Apr 9, 2018

In the bike shedding department, I didn’t see any reactions to @chrisdone’s suggestion of “pitype”. It’s googlable and one letter shorter than foreach. When you see it for the first time it kind of begs you to google it.

@glaebhoerl

This comment has been minimized.

glaebhoerl commented Apr 9, 2018

(The word "pi" would bother me less if we were actually following precedent by adopting it, but as far as I'm aware, none of the major dependently typed languages use it in their actual syntax.)

@Centril

This comment has been minimized.

Centril commented Apr 9, 2018

@glaebhoerl I think that is a factor of that in Agda and Idris, dependent types were there from the start, and so they have the nice syntax for dependent types where you just say {A: Set} -> (x: A) -> (n: Nat) -> Vec A n. But unfortunately we can't use (n: Nat) -> .. as discussed above. I'm not familiar with the syntax in Coq. I'm curious, are there any languages which added dependent types after the fact, and if so, what did they do / use as syntax?

@int-index

This comment has been minimized.

Contributor

int-index commented Apr 9, 2018

After some reflection, my view on pi, foreach and forall is that the two latter ones are too close together to not cause confusion between dependent and parametric modes.

  1. I disagree with the assumption that this confusion will be caused by naming — in general, people don't have the right intuition for relevance/irrelevance and its implications, so the confusion will be there either way. By using similar names we are more honest with the programmer, not trying to present those language features as completely different things.

  2. Would you agree that using similar keywords for similar concepts is more appropriate than using completely different keywords for similar concepts? Pondering the difference between the words forall and foreach can provide deeper intuition about the actual distinction between those quantifiers, while thinking about the difference between forall and pitype ends quickly as "they're not similar at all".

In other words, when I imagine explaining dependent types to a colleague, I feel more comfortable saying "foreach is like forall but relevant" than "pitype is like forall but relevant", as in the former case there's a neat parallel between the concepts and their names, while in the latter case only the concepts are subtly different, but not the names.

We have a similar case with data type declarations, type families, and data families — the name data family is neatly a hybrid between the names type family and data, so I can explain data families as "injective & generative type families" while still maintaining that each data instance is just like a regular data declaration.

@Centril

This comment has been minimized.

Centril commented Apr 9, 2018

@int-index You make some compelling arguments.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Apr 16, 2018

The committee has decided to table this proposal until there is a more crying need. The main motivation for writing this was to put the syntax in #81 in context, just to make sure we weren't painting ourselves into a corner. Even without acceptance, the existence of this proposal shows that #81 is forward-compatible. Thus this proposal will be marked dormant until we're closer to actually having dependent types.

@3noch

This comment has been minimized.

3noch commented Apr 18, 2018

Just to throw it out there: forevery

@davemenendez

This comment has been minimized.

davemenendez commented Apr 21, 2018

I agree the arguments against pi as the syntax for relevant quantifiers. In general, keywords should suggest the name of a thing rather than the name of the syntax used in some other context. (I dislike Python's lambda keyword for the same reason.)

I like foreach, because it suggests a similarity to forall while having the sense of treating things individually instead of collectively. However, if the similarity is judged too confusing, I suggest given as an alternative, as it suggests having access to something. For example, given k. k -> Type.

@ollef

This comment has been minimized.

ollef commented Jun 21, 2018

This is perhaps tangential, but is there anywhere I can read more about matchability in Haskell, and especially the story for it in dependent Haskell? Several dependently typed systems have had inconsistencies in the past due to assuming injectivity of type constructors (see Idris issue idris-lang/Idris-dev#3687, which links to similar issues in Agda and Lean). Is there some special sauce that makes it work out in Haskell?

@adamgundry

This comment has been minimized.

Contributor

adamgundry commented Jun 21, 2018

@ollef Haskell's term and type languages are already inconsistent as logics (because of general recursion and type-in-type, for starters). Injectivity of type constructors merely gives another way to write looping terms/types, but we have several ways already!

We'd be in trouble (type safety would be broken) if the coercion language was inconsistent, but the coercion language is already much more restricted than the type or term languages.

@Ericson2314

This comment has been minimized.

Ericson2314 commented Aug 3, 2018

Can explicit matchablity in type families replace data families? (I didn't see this discussed in the thesis, which surprised me.)

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Aug 4, 2018

The syntax in my thesis doesn't allow for this: type families are implemented via lambdas, which are always unmatchable. I'm not sure precisely how data families would fit in, but I'm sure there's a way.

@Ericson2314

This comment has been minimized.

Ericson2314 commented Aug 4, 2018

I forgot to say I was thinking particularly about associated data families. This is stretch from how things work today, and I believe what your thesis proposes, but say given:

class A x where
  type Foo x :: SomeK
class B x where
  data Bar x :: SomeK

we have top level signatures:

Foo :: forall x. A x => x -> SomeK
Bar :: forall x. A x '=> x '-> SomeK
@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Aug 4, 2018

You're right that data families are matchable and that type families aren't, but there are still several problems:

  • You're assuming constrained type families here. It's a fine assumption, but it's different than what we have today (and nothing in my thesis suggests it).

  • The types you write aren't quite right. I would write

    Foo :: forall k. forall (x :: k) -> A x => SomeK
    Bar :: forall k '. forall (x :: k) '-> A x '=> SomeK
    

    though I'm still not quite sure all the quantifiers are matchable in the data family case. Would need to think a bit harder.

  • There is no way to implement Bar based directly on features in my thesis. I don't think.

@Ericson2314

This comment has been minimized.

Ericson2314 commented Aug 4, 2018

Yes, that is the big assumption, and yes sorry, those types are the right ones I agree. Is there any literature on constrained type families for Haskell? I'd hope that would be (mostly) backwards compatible. I like it for consistency with class functions, even though it makes associated type/data families farther from their standalone counterparts.

@goldfirere

This comment has been minimized.

Contributor

goldfirere commented Aug 5, 2018

The Constrained Type Families paper has the details, but not in the context of dependent types.

@bravit bravit added the Proposal label Nov 11, 2018

@bravit bravit removed the Proposal label Dec 3, 2018

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