linearity-lab

This work-in-progress project aims to develop a library for embedding (variations of) linear/non-linear languages in Haskell, and interpreting them in suitable categories to write interesting programs.

For a quick taste of this library, the following code defines the type of lists in an ordered linear language, together with some basic operations:

-- `L a` is the fixed-point of `Sum One (a ** L a)` where `Sum` is the coproduct
-- type and `**` is the linear product type.
type L :: LType -> LType
type L (a :: LType) = LFix (L_ a)
-- `L_` is essentially the function `L_ a = One \`Sum\` (a ** x)`. In Haskell
-- we need the trick of using a 'dummy type' to define functions `LType -> LType`
-- at the type level.
data L_ (a :: LType)
type instance Decode (L_ a) x = One `Sum` (a ** x)
-- The language features needed for linear lists
type HasList exp = (HasCtx exp, HasLFix exp, HasLProd exp, HasCoProd exp)
-- The empty linear list
nilL :: (HasList exp, IsWF a) => exp '[] (L a)
nilL = con (inl l1)
-- Constructing a linear list from a head and a tail
consL :: (HasList exp, IsWF a, CApp ctx1 ctx2 ctx)
 => exp ctx1 a -> exp ctx2 (L a) -> exp ctx (L a)
consL h t = con (inr (h ** t))
-- Constructing a singleton linear list
singL :: (HasList exp, IsWF a, CApp ctx '[] ctx)
 => exp ctx a -> exp ctx (L a)
singL x = consL x nilL
-- Matching the two cases of a list
matchL :: (HasList exp, IsWF ctx, AllWF '[a, t])
 => exp ctx (L a)
 -> exp '[] t
 -> (exp '[ '(0, a) ] a -> exp '[ '(1, L a) ] (L a)
 -> exp '[ '(0, a), '(1, L a) ] t)
 -> exp ctx t
matchL l n c = lcase (des l) (\o -> unpack1 o n) (\ht -> unpack ht (\h t -> c h t))
-- Embedding a list as an endo-function on list
cayley :: (HasList exp, HasLFun exp, IsWF a, IsWF ctx)
 => exp ctx (L a) -> exp ctx (L a -* L a)
cayley xs = matchL xs (abs $ \x -> x) (\x xs -> abs (\ys -> consL x (cayley xs ^ ys)))
-- List concatenation
appL :: (HasList exp, HasLFun exp, IsWF a, CApp ctx1 ctx2 ctx)
 => exp ctx1 (L a) -> exp ctx2 (L a) -> exp ctx (L a)
appL xs ys = cayley xs ^ ys

The ordered linear type system ensures that all list payloads are consumed exactly once and in the correct order. Consequently, the operations above can be interpreted in the monoidal category of endofunctors and composition, giving us the free monad:

type Free :: (Type -> Type) -> (Type -> Type)
type Free f = FctLTy_ (L (Fct f))
injFree :: forall f x . Functor f => f x -> Free f x
injFree = asFctMap @'[Fct f] $ \(Vars c) -> singL c
joinFree :: forall f x . Functor f => Free f (Free f x) -> Free f x
joinFree = asFctMap @[L (Fct f), L (Fct f)] $ \(Vars (c, k)) -> appL c k

If you are interested, the file src/LinearityLab/Programs/List.hs is a good starting point for exploring this library.

At the moment, the following languages are implemented:

• ordered linear/non-linear languages and their semantics in (1) the endofunctor category and (2) the category of types and functions. This is my main motivation for writing this library: programming with endofunctors via an ordered linear language.

• call-by-push-value languages and their semantics in the Eilenberg-Moore category of a monad.

In current implementations, the non-linear sub-language is fixed to be Haskell types and functions. In the future I hope to relax this restriction and also implement (symmetrically) linear languages.

Source code structure:

• src/LinearityLab/Syntax contains type connectives defined as Haskell type-classes;

• src/LinearityLab/Semantics contains implementations of type connectives, such as the semantics in the endofunctor category and the semantics in ordinary types;

• src/LinearityLab/Programs contains some functional data structure written in linear languages (and thus can be interpreted in suitable monoidal categories).