Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

What are lifted and unlifted product types in Haskell?

Tags:

types

haskell

I recently came across the term "lifted product type" recently, as contrasted to an unlifted one.

I can't recall the context, but I see there are other questions on Stack Overflow asking about the disadvantages of unlifted product types (example).

I know more or less what a product type is. It's something like (a, b) or Foo a b c that corresponds roughly to a Cartesian product from set theory.

What do the terms "lifted" and "unlifted" mean in this context?

like image 359
jml Avatar asked Oct 11 '16 19:10

jml


2 Answers

From the GHC docs:

“lifted” type means that terms of that type may be bottom.

“boxed” type means that a value is represented by a pointer to a heap object.

Some implications include:

  • A lifted type is boxed (but not necessarily the other way - check out the link above for more)
  • Unboxed types cannot have thunks (since those are pointers to data telling you how to produce the value), so no laziness. They really just hold values. This also means they can be faster.
  • Polymorphism does not play with unlifted types. Whenever you see a type variable, all the types involved are unlifted. Something like id 0 :: Int# does not work. Check out this answer to see how you can (since GHC 8.0) sometimes maneuver around this.

Note that you can create unlifted products in GHC using MagicHash and UnboxedTuples extensions (although I don't think they play well with GHCi):

{-# LANGUAGE MagicHash, UnboxedTuples #-}

extGCD :: Int -> Int -> (# Int, Int, Int #)
extGCD a 0 = (# 1, 0, a #)
extGCD a b = let (q, r) = a `quotRem` b
                 (# s, t, g #) = extGCD b r
             in  (# t, s - q * t, abs g #)

With the exception of this extension, I believe the only unlifted types you will find are in GHC.Exts and are the primitive types. There is some discussion to allow custom unlifted data types to be integrated into GHC here.

One final remark: while lifted types have kind *, unlifted types have kind #. This answer to the question linked in the comments goes into more detail about this.

like image 160
Alec Avatar answered Nov 16 '22 02:11

Alec


From the GHC documentation:

Lifted

A type is lifted iff it has bottom as an element.

A value of a lifted type can be bottom. That is, it can be undefined, or perhaps a computation that never finishes, or one that throws an exception.

Meanwhile, unlifted types do not have those potentially troublesome extra values. This can be useful in a purely "semantic" level (if you don't want those extra values) and it can also facilitate more efficient implementations by reducing costly indirections. A GHC optimization called the worker-wrapper transformation exploits this (see section 5.1 of the linked paper).

Lifted and unlifted types have different kinds. Lifted types live in *, unlifted types in #.

Currently GHC doesn't let you define your own complex unlifted datatypes easily. But there are proposals to allow for that.

like image 27
danidiaz Avatar answered Nov 16 '22 03:11

danidiaz