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.

Unsafe Coersions

coerce :: a %1 -> b

Linearly typed unsafeCoerce

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

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. (a %p -> b %q -> c) %1 -> a %1 -> b %1 -> c

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. (a %p -> b %q -> c %r -> d) %1 -> a %1 -> b %1 -> c %1 -> d

Like toLinear but for three-argument functions