Simple.Pure

We have simple linear functions and simple linear data structures that illustrate the basic concepts of how the type checker of GHC with linear types behaves. The goal of this is to be a ridiculously simple tutorial on the basics of linear types.

Simple linear functions

linearIdentity :: a %1 -> a

linearSwap :: (a, a) %1 -> (a, a)

nonLinearSubsume :: (a, a) -> (a, a)

linearPairIdentity :: (a, a) %1 -> (a, a)

linearIdentity2 :: a %1 -> a

nonLinearPair :: a -> (a, a)

nonLinearPair2 :: a -> (a, a)

nonLinearTriple :: a -> (a, (a, a))

regularIdentity :: a -> a

(#.) :: (b %1 -> c) -> (a %1 -> b) -> a %1 -> c infixr 9

linearCompose :: (a, a) %1 -> (a, a)

Linear functions with user data types

data LinearHolder a where

Constructors

LinearHolder :: a -> LinearHolder a

linearHold :: a %1 -> LinearHolder a

linearHoldExtract :: LinearHolder a %1 -> a

linearIdentity3 :: a %1 -> a

data LinearHolder2 where

Constructors

LinearHolder2 :: a -> b -> LinearHolder2

linearHold' :: a %1 -> LinearHolder2

data ForcedUnlinear a where

Constructors

ForcedUnlinear :: a -> ForcedUnlinear a

forcedLinearPair :: ForcedUnlinear a %1 -> (a, a)

demote :: (ForcedUnlinear a %1 -> b) -> a -> b

promote :: (a -> b) -> ForcedUnlinear a %1 -> b