What is Levity polymorphism

by

Note: This answer is based on very recent observations on Levity discussions. Everything concerning Levity polymorphism is currently only implemented in the GHC 8.0 release candidates and as such subject to change (see #11471 for example).

TL;DR: It’s a way to make functions polymorphic over lifted and unlifted types, which is not possible with regular functions. For example the following code doesn’t type check with regular poly­mor­phi­sms, since Int# has kind #, but the type variables in id have kind *:

{-# LANGUAGE MagicHash #-}

import GHC.Prim

example :: Int# -> Int# 
example = id            -- does not work, since id :: a -> a

Couldn't match kind ‘*’ with ‘#’
When matching types
  a0 :: *
  Int# :: #
Expected type: Int# -> Int#
  Actual type: a0 -> a0
In the expression: id

Note that (->) still uses some magic.

Before I start to answer this question, let us take a step back and go to one of the most often used functions, ($).

What is ($)‘s type? Well, according to Hackage and the report, it’s

($) :: (a -> b) -> a -> b

However, that’s not 100% complete. It’s a convenient little lie. The problem is that polymorphic types (like a and b) have kind *. However, (library) developers wanted to use ($) not only for types with kind *, but also for those of kind #, e.g.

unwrapInt :: Int -> Int#

While Int has kind * (it can be bottom), Int# has kind # (and cannot be bottom at all). Still, the following code typechecks:

unwrapInt $ 42

That shouldn’t work. Remember the return type of ($)? It was polymorphic, and polymorphic types have kind *, not #! So why did it work? First, it was a bug, and then it was a hack (excerpt of a mail by Ryan Scott on the ghc-dev mailing list):

So why is this happening?

The long answer is that prior to GHC 8.0, in the type signature ($) :: (a -> b) -> a -> b, b actually wasn’t in kind *, but rather OpenKind.
OpenKind is an awful hack that allows both lifted (kind *) and
unlifted (kind #) types to inhabit it, which is why (unwrapInt $ 42)
typechecks.

So what is ($)‘s new type in GHC 8.0? It’s

($) :: forall (w :: Levity) a (b :: TYPE w). (a -> b) -> a -> b
-- will likely change according to Richard E.

To understand it, we must look at Levity:

data Levity = Lifted | Unlifted

Now, we can think of ($) as having either one of the following types, since there are only two choices of w:

-- pseudo types
($) :: forall a (b :: TYPE   Lifted). (a -> b) -> a -> b
($) :: forall a (b :: TYPE Unlifted). (a -> b) -> a -> b

TYPE is a magical constant, and it redefines the kinds * and # as

type * = TYPE Lifted
type # = TYPE Unlifted

The quantification over kinds is also fairly new and part of the integration of dependent types in Haskell.

The name Levity polymorphism comes from the fact that you now can write polymorphic functions over both lifted and unlifted types, something that wasn’t allowed/possible with the previous poly­mor­phism restrictions. It also gets rid of the OpenKind hack at the same time. It’s really “just” about this, handling both kinds of kinds.

By the way, you’re not alone with your question. Even Simon Peyton Jones said that there’s a need for a Levity wiki page, and Richard E. (the current implementer of this) stated that the wiki page needs an update on the current process.

References

More Related Contents:

  1. Haskell \p -> not takeWhile
  2. Sum of two numbers with function in haskell
  3. How to group similar items in a list using Haskell?
  4. Monads with Join() instead of Bind()
  5. How do I deal with many levels of indentation?
  6. Memoization in Haskell?
  7. What does the “@” symbol mean in reference to lists in Haskell?
  8. Wrong IO actions order using putStr and getLine
  9. New state of the art in unlimited generation of Hamming sequence
  10. Difference between `data` and `newtype` in Haskell
  11. How do functors work in haskell?
  12. double stream feed to prevent unneeded memoization?
  13. Currying subtraction
  14. Defining a new monad in haskell raises no instance for Applicative
  15. What are Alternative’s “some” and “many” useful for?
  16. Lambda for type expressions in Haskell?
  17. Check whether a type is an instance of Show in Haskell at runtime?
  18. Pattern matching identical values
  19. Composing Monads v. Applicative Functors
  20. Abusing the algebra of algebraic data types – why does this work?
  21. Why is Haskell (sometimes) referred to as “Best Imperative Language”?
  22. What does the : infix operator do in Haskell?
  23. Monoidal Functor is Applicative but where is the Monoid typeclass in the definition of Applicative?
  24. How to return a pure value from a impure method
  25. How to convert Unicode Escape Sequence to Unicode String in Haskell
  26. Haskell Constraint is no smaller than the instance head
  27. Can I match a data constructor wildcard in Haskell?
  28. Is there, in Haskell, something similar to sub-guards?
  29. What is the Comonad typeclass in Haskell?
  30. Is Haskell’s mapM not lazy?

Leave a Comment