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

Pi types instead of proxy types #3137

Open
paf31 opened this issue Oct 26, 2017 · 16 comments

Comments

Projects
None yet
7 participants
@paf31
Copy link
Member

commented Oct 26, 2017

Instead of proxy types, I would like to consider adding pi types, as an alternative to forall which requires explicit type application.

Pros

  • Unlike GHC's type applications, the order of type arguments in a forall is still irrelevant.
  • No runtime Proxy-passing needed
  • I don't think this has quite the same risk of kind issues as proxies (although I'm not fully sure yet)

Possible Syntax

Π is a new type former which binds a type variable. It is introduced with Λ. and eliminated with @ (which mirrors the current proxy syntax).

class IsSymbol (s :: Symbol) where
  reflectSymbol :: Πs. String

shoutSymbol :: Πs. IsSymbol s => String
shoutSymbol = Λ. toUpper (reflectSymbol @s)

@paf31 paf31 added the typechecker label Oct 26, 2017

@paf31 paf31 added this to the Ideas milestone Oct 26, 2017

@joneshf

This comment has been minimized.

Copy link
Member

commented Oct 26, 2017

I'm going to be the first person to say that we need non-unicode alternatives for this. We can do like we do for forall and -> and whatever and accept unicode as an alternative, but I'll fight vehemently for a non-unicode way to write the same syntax.

@garyb

This comment has been minimized.

Copy link
Member

commented Oct 26, 2017

Even though I loves my unicodes, I'm with you on that @joneshf.

@paf31

This comment has been minimized.

Copy link
Member Author

commented Oct 26, 2017

I totally agree, I just couldn't think of one :)

@joneshf

This comment has been minimized.

Copy link
Member

commented Oct 28, 2017

Sorry for immediately bikeshedding on the syntax of it.

@chexxor

This comment has been minimized.

Copy link
Contributor

commented Oct 28, 2017

Would you guess this would not make it in 1.0? My guess is its implementation is complicated. This would be a breaking change, I guess.

@rightfold

This comment has been minimized.

Copy link
Contributor

commented Dec 2, 2017

Π and Λ are identifiers, and λ for lambdas was also rejected :trollface:

@chexxor

This comment has been minimized.

Copy link
Contributor

commented Mar 7, 2018

Would this mean the Proxy short-hand syntax would need to choose a symbol different than @, which would be used for pi-types?
Currently, the @ for Proxy short-hand has been removed due to kind issues, discussed in issues linked here: #3178, which means @ is free again! :)

@hdgarrood

This comment has been minimized.

Copy link
Member

commented Mar 24, 2019

If Π binds a type variable, then wouldn't it shadow the s bound by the IsSymbol class declaration in your example, making reflectSymbol unusable (because it doesn't reference the class's s?)

@natefaubion

This comment has been minimized.

Copy link
Contributor

commented Mar 24, 2019

GHC has explicit forall a -> now (no dot).

class IsSymbol (s :: Symbol) where
  reflectSymbol :: forall s -> String

shoutSymbol :: forall s -> IsSymbol s => String
shoutSymbol = toUpper (reflectSymbol @s)

https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0035-forall-arrow.rst

@joneshf

This comment has been minimized.

Copy link
Member

commented Mar 24, 2019

That seems like a really unfortunate syntax to choose. Discerning an implicit type variable from an explicit type variable requires reading all the way past the type variable itself. Hopefully we don't decide to follow suit.

@natefaubion

This comment has been minimized.

Copy link
Contributor

commented Mar 24, 2019

FWIW, it was punted for a while due to syntax issues and then added because no-one could come up with something better 😆

@garyb

This comment has been minimized.

Copy link
Member

commented Mar 24, 2019

@hdgarrood

This comment has been minimized.

Copy link
Member

commented Mar 24, 2019

I guess the obvious alternative is to reserve pi as a keyword and write shoutSymbol :: pi s. IsSymbol s => String. That said, I’d suggest leaving syntax aside for now because I think this proposal could stand to be quite a bit more fleshed out than it currently is first.

I think what’s being considered here would have to be quite a bit larger in scope than the GHC feature discussed in that blog post because it sounds to me like there are a number of type system features which GHC Haskell has and which PureScript doesn’t, but which (afaict) we would need to have for this to make sense: in particular, kind polymorphism, merging types and kinds, and GADTs. That blog post discusses being able to annotate kinds which could already exist internally during type checking but which couldn’t previously be written out, but I think we are quite far away from these kinds even being able to exist internally in PureScript as things stand right now?

I’m not sure if my concern here is justified (since I don’t know a lot about dependent types), but I am a little concerned about where adding features like this would take us longer term; I’d prefer not to add dependent typing features one by one if that eventually leads us to a point where we have a hodgepodge of features which don’t really work fantastically well together. If we want a strict, practical, dependently typed language which compiles to JS, should we not just be using Idris?

@joneshf

This comment has been minimized.

Copy link
Member

commented Mar 24, 2019

in particular, kind polymorphism, merging types and kinds, and GADTs

Why do we need all of these for pi types? Doesn't Dhall have a similar situation without requiring these three things (it does have kind polymorphism now, but didn't before and you had to explicitly apply types)?

If we want a strict, practical, dependently typed language which compiles to JS, should we not just be using Idris?

This sort of reasoning doesn't work because you can't "just use Idris." You'd have to throw away every single thing you've written in PS and rebuild it in Idris. You'd have to sell all the other people that interact with the code on Idris. You'd have to throw away your PS infrastructure and tooling and rebuild it in Idris. Idris isn't PS++, and we can't just shove people off to it when we don't want to implement something.

Drawing a line in the sand for what a language will support is good; suggesting a non-alternative as an excuse for not implementing something is not. I.e. if we don't want pi types, we should be fine with that decision. We don't need to make excuses for having that decision.

@hdgarrood

This comment has been minimized.

Copy link
Member

commented Mar 25, 2019

Why do we need all of these for pi types?

I'm referring to the blog post which @garyb linked. It's still not entirely clear to me what is meant in our particular context by "pi types", but that blog post at least relies heavily on GHC Haskell having the features I mentioned.

We don't need to make excuses for having that decision.

Just to clarify, my stance is that:

  1. if a language is going to have dependent types, I think it should probably be designed from the start to have them. If you wait until you have a large ecosystem, set of principles for what is idiomatic and which features are appropriate to use in which situations and so on, and only then try to add DTs, you may well end up with an awkward design, because (at least if you look at Idris and how its standard library and ecosystem diverges from ours) it seems that dependent types have big implications for all of these things.
  2. I don't think it makes sense to try to fill a niche which has already been filled (in this case, by Idris).
  3. the less code we have inside the compiler, the easier the compiler is to maintain, which I would argue translates pretty directly to it being nicer to use (because we have more time and energy to devote to things like bug fixes, performance, or error messages).

I feel that the above is a coherent argument for not adding dependent typing features, and does not constitute "making excuses". (I don't really like this language honestly, I think it risks coming across as judgemental).

Of course it's very possible that the implications of this change aren't nearly as large as I'm making them out to be, and I'm happy to be corrected if so.

I think it's also worth pointing out that everyone is already using proxies for this sort of thing, and although they do have a small runtime cost, they do pretty much do their job fine (as always, I'm very happy to be corrected if I'm missing something here). If we end up with a situation where some libraries use proxies and others use pi types for passing type parameters as arguments to functions, and then everyone has to learn how to use both, I think that's possibly even a slightly worse situation than the one we're in now.

@joneshf

This comment has been minimized.

Copy link
Member

commented Mar 26, 2019

I feel that the above is a coherent argument for not adding dependent typing features, and does not constitute "making excuses".

I agree, and I never objected to that part. It was the jump from "let's add pi types" to "Idris has dependent types and compiles to JS, so just use that." As a user, it's kind of a slap in the face to ask for pi types and hear that you should use Idris instead, for many reasons.

I'm sorry I said the thing about making excuses. It does sound kind of rude. The point I'm trying to make is that we should justify features by what we want or don't want. Some other language having a feature shouldn't have much weight in the decision because a user of languages can't just pick and choose a different language that easily. If we want something, we want it. If we don't want something, we don't want it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.