| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Unsafe.Linear
Contents
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
- coerce :: forall a b. a %1 -> b
- toLinear :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1) (b :: TYPE r2) p x. (a %p -> b) %1 -> a %x -> b
- 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
- 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
- toLinearN :: forall n f g. ToLinearN n f g => f %1 -> g
- class ToLinearN n f g where
Unsafe Coercions
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[]) $ unsafeLinearityProofN2(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.