| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Data.Elevator
Description
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 Methods 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 Methods levCoerce# :: a -> Lazy a Source # | |
levCoerce :: LevitySubsumption a b => a -> b Source #
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)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.
Methods
levCoerce# :: a -> b Source #