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

Kind polymorphism #1763

Open
paf31 opened this issue Dec 27, 2015 · 11 comments

Comments

Projects
None yet
8 participants
@paf31
Copy link
Member

commented Dec 27, 2015

No description provided.

@paf31 paf31 added this to the 0.9.0 milestone Dec 27, 2015

@paf31 paf31 self-assigned this Dec 27, 2015

paf31 added a commit that referenced this issue Dec 27, 2015

paf31 added a commit that referenced this issue Dec 27, 2015

@LiamGoodacre

This comment has been minimized.

Copy link
Member

commented Feb 16, 2016

Is it worth starting a list of libraries that will benefit from this?

Off the top of my head I can think of:

@paf31 paf31 modified the milestones: 0.9.0, 0.10.0 Apr 10, 2016

@rgrempel

This comment has been minimized.

Copy link

commented Jul 15, 2016

I believe that purescript-typeable would also benefit.

It could enable a switch to a polymorphically-kinded Typeable implementation, similar to the approach now used in Haskell.

@paf31

This comment has been minimized.

Copy link
Member Author

commented Dec 24, 2016

I had a bit of a strange idea for an alternative to kind polymorphism.

Instead of adding more machinery to the kind level, we could go the other way and make the type-level language dynamically typed. Here is how this could work:

  • Just like dynamic languages track types at runtime, by tagging values, our types will be tagged with kinds.
  • Instead of inferring and checking kinds, we simply evaluate kinds during type-checking. For example, whenever we see a type application f a, we look at the tag on f and make sure it is a function, and then apply that function to the tag on a.
  • This will allow us to define things like a Proxy type constructor which accepts types of any kind.
  • Things like List Maybe will still be ill-kinded, but this will be caught during type-checking, since the kinds in question do not evaluate to *.
  • This will allow some relatively crazy type definitions like type Omega a = a a, but that's fine, since any issues will be caught during type-checking anyway (Omega List is bad, but Omega Proxy is fine). Generally, type definitions will not get checked (except to make sure that data declarations actually contain data of kind *)
  • Type checking might diverge, but it already does anyway because of infinite instances.
  • This should fix another issue (#2103 - "Prefer kind errors to type errors where both occur"). Generally, I think this can improve our kind-related errors quite a bit, since they will essentially become evaluation traces.

Of course, this is a bit at odds with other things going on at the moment, namely @LiamGoodacre's work on user-defined kinds, but I think we can incorporate that work at the same time. Specifically, instead of defining the kind of a type, we just declare a type with its tag.

So, what do people think?

@jdegoes

This comment has been minimized.

Copy link

commented Dec 24, 2016

At first glance, I really like it. 👍

@LiamGoodacre

This comment has been minimized.

Copy link
Member

commented Dec 24, 2016

I think this has the potential to be really awesome. Coin the term dynamically-kinded types? 😄

Though I am wondering how this will play with type classes - I suspect in some (unusual) cases it may be undecidable to select an instance if the type class doesn't have fixed kinds for its arguments - but I need to explore that more and come up with a good example.

@LiamGoodacre

This comment has been minimized.

Copy link
Member

commented Dec 25, 2016

Actually I think my previous concerns would manifest with poly kinds too.

@Pauan

This comment has been minimized.

Copy link

commented Dec 25, 2016

@paf31 I like it.

It also potentially paves the way for more dependent-type stuff later.

I think it's okay to have kinds/types be dynamically typed, because ultimately the type checker is running at compile time, so any "dynamic kind" errors are caught at compile-time.

@jjl

This comment has been minimized.

Copy link

commented Dec 29, 2018

One of my libraries would really benefit from either approach. It would be nice to nail down a spec for implementation.

@EpicOrange

This comment has been minimized.

Copy link

commented Apr 5, 2019

Hey! Data.Exists is slightly non-useful without poly kinds (can't add any constraints to the Exists type), so I'm interested in seeing progress here! Is there anything against @paf31's 'dynamically-kinded' types (other than the diverging typechecking issue)?

@LiamGoodacre

This comment has been minimized.

Copy link
Member

commented Apr 9, 2019

@EpicOrange What do you mean by "can't add any constraints to the Exists type"?
If you're talking about a Constraint kind like in Haskell, then poly-kinds wouldn't give you that.
If you're talking about constraints on data-constructors, then you'd want (something like) GADTs - which is also unrelated to poly-kinds.
Or have I misunderstood?

@garyb

This comment has been minimized.

Copy link
Member

commented Apr 10, 2019

@EpicOrange You can have constrained existentials even without using Exists too with an alternate encoding:

newtype Boxed = Boxed (∀ r. (∀ a. Show a  a  r)  r)

mkBoxed   a. Show a  a  Boxed
mkBoxed a = Boxed \unbox → unbox a

showBoxed  Boxed  String
showBoxed (Boxed f) = f show
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.