Data.Elevator.Internal

The kind of boxed, lifted types, for example [Int] or any other user-defined data type.

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.

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.

Re-use existing code taking arguments lazily to take arguments Strictly by coercing with levCoerce.Example: even can be re-used on Strict Int:

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

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:

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

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)

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.