Safe Haskell | Safe-Inferred |
---|---|

Language | Haskell2010 |

This module doesn't respect the PVP! Breaking changes may happen at any minor version (^>= *.*.m.*)

## Synopsis

- type LiftedType = Type
- type U = UnliftedType
- type L = LiftedType
- newtype Strict (a :: LiftedType) where
- Strict_ :: Any @UnliftedType -> Strict a

- toStrict# :: a -> Strict a
- fromStrict# :: Strict a -> a
- pattern Strict :: a -> Strict a
- newtype Lazy (a :: UnliftedType) where
- Lazy_ :: Any @LiftedType -> Lazy a

- toLazy# :: a -> Lazy a
- fromLazy# :: Lazy a -> a
- pattern Lazy :: a -> Lazy a
- levCoerce :: LevitySubsumption a b => a -> b
- class LevitySubsumption (a :: TYPE (BoxedRep l)) (b :: TYPE (BoxedRep r)) where
- levCoerce# :: a -> b

# Documentation

type LiftedType = Type Source #

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

or any other
user-defined data type.

type U = UnliftedType Source #

type L = LiftedType Source #

newtype Strict (a :: LiftedType) 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.

Strict_ :: Any @UnliftedType -> Strict a |

#### Instances

LevitySubsumption (Strict a :: TYPE UnliftedRep) (a :: LiftedType) Source # | |

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

fromStrict# :: Strict a -> a Source #

newtype 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.

Lazy_ :: Any @LiftedType -> Lazy a |

#### Instances

LevitySubsumption (a :: UnliftedType) (Lazy a :: TYPE LiftedRep) 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 #