Safe Haskell | None |
---|---|

Language | Haskell2010 |

Near zero-cost coercions between lifted and boxed unlifted types.

Turn any lifted type into an unlifted boxed type with `Strict`

, eagerly
forcing any wrapped computation in the syntactic binding context.

Turn any unlifted boxed type into a lifted type with `Lazy`

, suspending any
wrapped computation until the `Lazy`

is matched upon.

Re-use existing code by coercing functions that can be generalised according
to the levity polymorphism subkinding law `Unlifted <: Lifted`

with
`levCoerce`

.

## Synopsis

- type UnliftedType = TYPE UnliftedRep
- type LiftedType = Type
- data Strict a :: UnliftedType where
- data Lazy (a :: UnliftedType) where
- levCoerce :: LevitySubsumption a b => a -> b
- class LevitySubsumption (a :: TYPE ('BoxedRep l)) (b :: TYPE ('BoxedRep r)) where
- levCoerce# :: a -> b

# Documentation

type UnliftedType = TYPE UnliftedRep #

The kind of boxed, unlifted values, for example `Array#`

or a user-defined
unlifted data type, using `-XUnliftedDataTypes`

.

type LiftedType = Type Source #

The kind of boxed, lifted types, for example `[Int]`

or any other
user-defined data type.

data Strict a :: UnliftedType where Source #

Turn a lifted data type into an unlifted one. Unlifted data types enjoy a call-by-value calling convention. E.g.,

let f :: (a :: UnliftedType) -> Int f _ = 42 in f (Strict (error "boom" :: Int))

Will error out with `"boom"`

.

Note however that most function definitions don't take argument types of kind
`UnliftedType`

. Use `levCoerce`

to work around that.

#### Instances

LevitySubsumption (Strict a :: UnliftedType) (a :: LiftedType) Source # | |

Defined in Data.Elevator.Internal levCoerce# :: Strict a -> a Source # |

data Lazy (a :: UnliftedType) where Source #

Turn an unlifted boxed type into a lifted one.
`Lazy a`

then enjoys a call-by-name calling convention. E.g.,

let f :: a -> Int f _ = 42 in f (Lazy (error "boom" :: Array# Int))

Will evaluate to `42`

and not error.

#### Instances

LevitySubsumption (a :: UnliftedType) (Lazy a :: Type) Source # | |

Defined in Data.Elevator.Internal levCoerce# :: a -> Lazy a Source # |

levCoerce :: LevitySubsumption a b => a -> b Source #

Re-use existing code taking arguments lazily to take arguments `Strict`

ly
by coercing with `levCoerce`

.Example: `even`

can be
re-used on `Strict Int`

:

`>>>`

True`levCoerce @(Int -> Bool) @(Strict Int -> Bool) even (Strict 42)`

More generally, any type of kind `UnliftedType`

can act as a ("is-a") type
of kind `LiftedType`

. This levity polymorphism subkinding axiom
`Unlifted <: Lifted`

is encoded in `LevitySubsumption`

and is lifted to
useful instances for `Strict`

, `Lazy`

and `(->)`

. Example with covariance in
the result type:

`>>>`

True`levCoerce @(Int -> Strict Bool) @(Strict Int -> Bool) (\x -> Strict (even x)) (Strict 42)`

A function from `Int`

to `Strict Bool`

can be called on a `Strict Int`

(e.g.,
the precondition strengthened) and the result can be coerced to `Bool`

(e.g.,
the postcondition weakened).

You can also keep on coercing in negative position of the function arrow, with the variance following polarity:

levCoerce @((Strict Int -> Int) -> Int) @((Int -> Strict Int) -> Int) (\f -> f (Strict 42)) (\x -> Strict x)

class LevitySubsumption (a :: TYPE ('BoxedRep l)) (b :: TYPE ('BoxedRep r)) where Source #

Similar to `Coercible`

, this type class models a subkinding relationship
between two types. The instances lift the `Unlifted <: Lifted`

sub-kinding
relationship to `TYPE`

, `Strict`

, `Lazy`

and then over function types.

Like for `Coercible`

, the instances of this type class should ultimately be
compiler-generated.

levCoerce# :: a -> b Source #