| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Data.Elevator.Internal
Description
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.
Constructors
| Strict_ :: Any @UnliftedType -> Strict a |
Instances
| LevitySubsumption (Strict a :: TYPE UnliftedRep) (a :: LiftedType) Source # | |
Defined in Data.Elevator.Internal Methods 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.
Constructors
| Lazy_ :: Any @LiftedType -> Lazy a |
Instances
| LevitySubsumption (a :: UnliftedType) (Lazy a :: TYPE LiftedRep) 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 #