Modulelinear-base-0.4.0Haskell2010

Unsafe.Linear

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.

1 class
5 values

Packagelinear-base-0.4.0
Exports6
LanguageHaskell2010
LicenceMIT
SourceLinear.hs

Unsafe Coercions

6 declarations

valuecoerce :: a %1 -> b

Linearly typed unsafeCoerce

valuetoLinear :: (a %p -> b) %1 -> a %x -> b

Converts an unrestricted function into a linear function

valuetoLinear2 :: (a %p -> b %q -> c) %1 -> a %x -> b %y -> c

Like toLinear but for two-argument functions

valuetoLinear3 :: (a %p -> b %q -> c %r -> d) %1 -> a %x -> b %y -> c %z -> d

Like toLinear but for three-argument functions

valuetoLinearN :: ToLinearN n f g => f %1 -> g

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

classclass ToLinearN (n :: Nat) (f :: TYPE rep) (g :: TYPE rep) where

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
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.

Instances1ToLinearN

(ToLinearN' ni f g, ni ~ ToINat n) => ToLinearN n f gDefined in linear-base-0.4.0 · Unsafe.Linear