Home » forums » LtU Forum

Programming languages with higher kinds?

Are there languages other than Haskell and Scala that have higher kinded type systems? Does O'Caml count now?

By Steven Shaw II at 2010-10-15 04:23 | LtU Forum | previous forum topic | next forum topic | other blogs | 8239 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Omega by Tim Sheard

Ωmega by Tim Sheard

By dmbarbour at Fri, 2010-10-15 04:28 | login or register to post comments

Yes...

...Ocaml counts, though I wouldn't exactly call it pleasant just yet. At ICFP, Jacque Garrigue reported that there was work underway to increase the amount of type inference done on programs with first-class modules, which will surely help a lot.

Also, Agda supports higher kinded programming, as does Coq.

By neelk at Fri, 2010-10-15 07:53 | login or register to post comments

Some

OCaml and other MLs do not provide higher kinds directly, but they can be emulated through the use of functors.

C++ has "template template arguments", which give you a form of higher-order type constructors. Since they are basically untyped, there arguably are no kinds, though.

Any language with type universes, like Coq or Agda, subsumes higher kinds. In these language, kinds are just types one level up, with the full expressive power of "ordinary" types, and there usually is an infinite tower of them.

There are also languages that collapse this tower, i.e. "type" (aka the kind "*") is just a type itself. These are even more expressive -- to the point that they are no longer logically consistent.

By Andreas Rossberg at Fri, 2010-10-15 09:25 | login or register to post comments

Ur by Adam Chlipala

Ur by Adam Chlipala.

By Petter Urkedal at Sat, 2010-10-16 14:58 | login or register to post comments