-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/
-- | Coerce between unlifted boxed and lifted types.
--
-- Near zero-cost coercions between unlifted boxed and lifted types.
-- There are 3 main ingredients to this library: (1) a newtype Strict
-- :: LiftedType -> UnliftedType, (2) a newtype Lazy ::
-- UnliftedType -> LiftedType, and (3) a coercion function
-- levCoerce to coerce existing functions into accepting
-- Strict wrapper.
@package data-elevator
@version 0.1.0.0
-- | This module doesn't respect the PVP! Breaking changes may happen at
-- any minor version (^>= *.*.m.*)
module Data.Elevator.Internal
-- | The kind of boxed, lifted types, for example [Int] or any
-- other user-defined data type.
type LiftedType = Type
type U = UnliftedType
type L = LiftedType
-- | 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.
newtype Strict (a :: LiftedType)
[Strict_] :: Any @UnliftedType -> Strict a
toStrict# :: a -> Strict a
fromStrict# :: Strict a -> a
pattern Strict :: a -> Strict a
-- | 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.
newtype Lazy (a :: UnliftedType)
[Lazy_] :: Any @LiftedType -> Lazy a
toLazy# :: a -> Lazy a
fromLazy# :: Lazy a -> a
pattern Lazy :: a -> Lazy a
-- | 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)
--
levCoerce :: LevitySubsumption a b => a -> b
-- | 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.
class LevitySubsumption (a :: TYPE (BoxedRep l)) (b :: TYPE (BoxedRep r))
levCoerce# :: LevitySubsumption a b => a -> b
instance Data.Elevator.Internal.LevitySubsumption a a
instance Data.Elevator.Internal.LevitySubsumption a a
instance Data.Elevator.Internal.LevitySubsumption (Data.Elevator.Internal.Strict a) a
instance Data.Elevator.Internal.LevitySubsumption a (Data.Elevator.Internal.Lazy a)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
instance (Data.Elevator.Internal.LevitySubsumption a2 a1, Data.Elevator.Internal.LevitySubsumption b1 b2) => Data.Elevator.Internal.LevitySubsumption (a1 -> b1) (a2 -> b2)
-- | 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.
module Data.Elevator
-- | The kind of boxed, unlifted values, for example Array# or a
-- user-defined unlifted data type, using -XUnliftedDataTypes.
type UnliftedType = TYPE UnliftedRep
-- | The kind of boxed, lifted types, for example [Int] or any
-- other user-defined data type.
type LiftedType = 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.
data Strict (a :: LiftedType)
pattern Strict :: a -> Strict a
-- | 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.
data Lazy (a :: UnliftedType)
pattern Lazy :: a -> Lazy a
-- | 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)
--
levCoerce :: LevitySubsumption a b => a -> b
-- | 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.
class LevitySubsumption (a :: TYPE (BoxedRep l)) (b :: TYPE (BoxedRep r))
levCoerce# :: LevitySubsumption a b => a -> b