linear-base-0.3.1: Standard library for linear types.
Safe HaskellSafe-Inferred
LanguageHaskell2010

Unsafe.Linear

Description

Unsafe coercions for linearly typed code.

Use this module to coerce non-linear functions to be linear or values bound linearly to be another type. All functions in this module are unsafe.

Hence:

  • Import this module qualifed as Unsafe.
  • Do not use this unless you have to. Specifically, if you can write a linear function f :: A %1-> B, do not write a non-linear version and coerce it.
Synopsis

Unsafe Coercions

coerce :: forall a b. a %1 -> b Source #

Linearly typed unsafeCoerce

toLinear :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2) p x. (a %p -> b) %1 -> a %x -> b Source #

Converts an unrestricted function into a linear function

toLinear2 :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (r3 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2) (c :: TYPE r3) p q x y. (a %p -> b %q -> c) %1 -> a %x -> b %y -> c Source #

Like toLinear but for two-argument functions

toLinear3 :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (r3 :: RuntimeRep) (r4 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2) (c :: TYPE r3) (d :: TYPE r4) p q r x y z. (a %p -> b %q -> c %r -> d) %1 -> a %x -> b %y -> c %z -> d Source #

Like toLinear but for three-argument functions

toLinearN :: forall n f g. ToLinearN n f g => f %1 -> g Source #

toLinearN subsumes the functionality of toLinear1, toLinear2, and toLinear3. In particular, toLinearN @n unsafely changes the multiplicities of the first n arrows from any multiplicity to any other multiplicity. To be explicit about how each multiplicity is being changed, you can use additional type arguments.

Examples

toLinearN @2 :: (a %m-> b %n-> Int) %1-> a %x-> b %y-> Int
toLinearN @3 @(_ %m-> _ -> _ %1-> _) @(_ %1-> _ %1-> _ %x-> _)
  :: (a %m-> b -> c %1-> d) %1-> (a %1-> b %1-> c %x-> d)
toLinear3 = toLinearN @3

class ToLinearN n f g where Source #

ToLinearN n f g means that f and g are the same with the possible exception of the multiplicities of the first n arrows.

Methods

unsafeLinearityProofN :: UnsafeEquality f g Source #

Given that f and g are the same, with the possible exception of the multiplicities of the first n arrows, unsafeLinearityProofN @n @f @g is a fake proof that f and g are identical. This is used primarily in the definition of toLinearN, but it can also be used, for example, to coerce a container of functions:

linearMany :: forall a b c. [a -> b -> c] %1-> [a %1-> b %1-> c]
linearMany = castWithUnsafe (applyUnsafe (UnsafeRefl []) $
  unsafeLinearityProofN 2 (a -> b -> c) (a %1-> b %1-> c))

applyUnsafe :: UnsafeEquality f g -> UnsafeEquality x y -> UnsafeEquality (f x) (g y)
applyUnsafe UnsafeRefl UnsafeRefl = UnsafeRefl

castWithUnsafe :: UnsafeEquality x y -> x %1-> y
castWithUnsafe UnsafeRefl x = x

The rather explicit handling of coercions seems to be necessary, unfortunately, presumably due to the way GHC eagerly rejects equality constraints it sees as definitely unsatisfiable.

Instances

Instances details
(ToLinearN' ni f g, ni ~ ToINat n) => ToLinearN n (f :: Type) (g :: Type) Source # 
Instance details

Defined in Unsafe.Linear