Safe Haskell	None
Language	GHC2024

SysL

Contents

Types
Values and boundaries
Syntax
Direct evaluator
Polynomial view
SMC SMC compiler
Process interpreter
Then as optic
Regression tests

Description

System L with polynomial types and These covariable boundaries.

This module rebuilds the original hand-rolled Loop (,) (->) interpreter as a circuits client:

User-facing types are promoted to Poly polynomials via SysLTy.
Command results are expressed with These boundaries, matching the inclusive tensor in Circuit.Channel.
The syntactic target is the free SMC SMC (->); boundaries use These at the value level.
A streaming reading is provided via Process.

The original four regression tests are preserved as testId, testThen, testIdLoop and testThenLoop.

Synopsis

data Ty
- = One
- | Times Ty Ty
- | Zero
- | Plus Ty Ty
- | Hom Ty Ty
- | GradedHom Ty [Ty]
- | Then Ty Ty
type family SysLTy (t :: Ty) :: Poly where ...
type family Domain (t :: Ty) where ...
data Val v
- = VUnit
- | VPair (Val v) (Val v)
- | VLeft (Val v)
- | VRight (Val v)
- | VFun (Val v -> Result v)
- | VGradedFun (Val v -> Result v)
- | VThen (Val v) (Val v -> Result v)
- | VEmbed v
type Output v = (Int, Val v)
type Result v = These (Output v) (Output v)
type Env v = [Val v]
data Command v = Cut (Term v) (Coterm v)
data Value v
- = Var Int
- | TensorIntro (Value v) (Value v)
- | PlusIntroL (Value v)
- | PlusIntroR (Value v)
- | HomComatch (Command v)
- | GradedHomComatch (Command v)
- | Lit (Val v)
data Term v
- = Embed (Value v)
- | Mu (Command v)
- | ThenComatch (Command v)
data Coterm v
- = Covar Int
- | Comu (Command v)
- | TensorMatch (Command v)
- | PlusMatch (Command v) (Command v)
- | HomCointro (Term v) (Coterm v)
- | GradedHomCointro (Term v) [Coterm v]
- | ThenCointro (Coterm v) (Coterm v)
evalCommand :: Command v -> Env v -> Result v
evalValue :: Value v -> Env v -> Val v
evalTerm :: Term v -> Env v -> These (Output v) (Val v)
evalCoterm :: Coterm v -> Env v -> Val v -> Result v
lookupEnv :: Int -> Env v -> Val v
class PolyVal (t :: Ty) where
- valToEval :: Val v -> Eval (SysLTy t) v
- evalToVal :: Eval (SysLTy t) v -> Val v
type SMCThese = SMC (,) (->)
commandToSMC :: Command v -> SMCThese (Env v) (Result v)
termToSMC :: Term v -> SMCThese (Env v) (These (Output v) (Val v))
cotermToSMC :: Coterm v -> SMCThese (Env v, Val v) (Result v)
evalProcess :: Term v -> Process (Env v) (Val v)
thenLens :: (Val v -> Val v) -> (Val v -> Val v -> Val v) -> Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v))
applyThen :: Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v)) -> Val v -> (Val v, Val v -> Val v)
testId :: Result ()
testThen :: Result Double
testIdLoop :: Result ()
testThenLoop :: Result Double

Types

data Ty Source #

User-facing SysL type syntax.

Constructors

One
Times Ty Ty
Zero
Plus Ty Ty
Hom Ty Ty
GradedHom Ty [Ty]
Then Ty Ty

Instances

Instances details

Eq Ty Source #
Instance details Defined in SysL Methods (==) :: Ty -> Ty -> Bool # (/=) :: Ty -> Ty -> Bool #
Show Ty Source #
Instance details Defined in SysL Methods showsPrec :: Int -> Ty -> ShowS # show :: Ty -> String # showList :: [Ty] -> ShowS #

type family SysLTy (t :: Ty) :: Poly where ... Source #

Promoted polynomial encoding of a SysL type.

Hom, Then and the graded variant are represented as monomial lenses / dependent optics, which is the natural polynomial reading of functions with a backward map.

Equations

SysLTy 'One = 'Const ()
SysLTy ('Times a b) = 'Prod (SysLTy a) (SysLTy b)
SysLTy 'Zero = 'Const Void
SysLTy ('Plus a b) = 'Sum (SysLTy a) (SysLTy b)
SysLTy ('Hom a b) = Mono (Domain a) (Domain b)
SysLTy ('Then a b) = Mono (Domain a) (Domain b)
SysLTy ('GradedHom a bs) = GradedPoly a bs

type family Domain (t :: Ty) where ... Source #

Closed value domain for a SysL type.

Equations

Domain 'One = ()
Domain ('Times a b) = (Domain a, Domain b)
Domain 'Zero = Void
Domain ('Plus a b) = Either (Domain a) (Domain b)
Domain ('Hom a b) = Domain a -> Domain b
Domain ('Then a b) = Domain a -> Domain b
Domain ('GradedHom a bs) = Domain a -> GradedResult bs

Values and boundaries

data Val v Source #

Runtime values, parametric in the opaque domain type v.

Constructors

VUnit
VPair (Val v) (Val v)
VLeft (Val v)
VRight (Val v)
VFun (Val v -> Result v)
VGradedFun (Val v -> Result v)
VThen (Val v) (Val v -> Result v)
VEmbed v

Instances

Instances details

Eq v => Eq (Val v) Source #
Instance details Defined in SysL Methods (==) :: Val v -> Val v -> Bool # (/=) :: Val v -> Val v -> Bool #
Show v => Show (Val v) Source #
Instance details Defined in SysL Methods showsPrec :: Int -> Val v -> ShowS # show :: Val v -> String # showList :: [Val v] -> ShowS #

type Output v = (Int, Val v) Source #

An output is a slot together with a value.

type Result v = These (Output v) (Output v) Source #

A result is now a covariable boundary using the inclusive These tensor.

This carries a residual output (slot >= 1).
That carries a focus output (slot 0).
These carries both residual and focus.

This follows the convention in Circuit.Channel: This is the feedback residual branch and That is the payload focus branch.

type Env v = [Val v] Source #

Input environment: de Bruijn indexed list of values.

Syntax

data Command v Source #

Constructors

Cut (Term v) (Coterm v)

Instances

Instances details

Show v => Show (Command v) Source #
Instance details Defined in SysL Methods showsPrec :: Int -> Command v -> ShowS # show :: Command v -> String # showList :: [Command v] -> ShowS #

data Value v Source #

Constructors

Var Int
TensorIntro (Value v) (Value v)
PlusIntroL (Value v)
PlusIntroR (Value v)
HomComatch (Command v)
GradedHomComatch (Command v)
Lit (Val v)

Instances

Instances details

Show v => Show (Value v) Source #
Instance details Defined in SysL Methods showsPrec :: Int -> Value v -> ShowS # show :: Value v -> String # showList :: [Value v] -> ShowS #

data Term v Source #

Constructors

Embed (Value v)
Mu (Command v)
ThenComatch (Command v)

Instances

Instances details

Show v => Show (Term v) Source #
Instance details Defined in SysL Methods showsPrec :: Int -> Term v -> ShowS # show :: Term v -> String # showList :: [Term v] -> ShowS #

data Coterm v Source #

Constructors

Covar Int
Comu (Command v)
TensorMatch (Command v)
PlusMatch (Command v) (Command v)
HomCointro (Term v) (Coterm v)
GradedHomCointro (Term v) [Coterm v]
ThenCointro (Coterm v) (Coterm v)

Instances

Instances details

Show v => Show (Coterm v) Source #
Instance details Defined in SysL Methods showsPrec :: Int -> Coterm v -> ShowS # show :: Coterm v -> String # showList :: [Coterm v] -> ShowS #

Direct evaluator

evalCommand :: Command v -> Env v -> Result v Source #

evalValue :: Value v -> Env v -> Val v Source #

evalTerm :: Term v -> Env v -> These (Output v) (Val v) Source #

evalCoterm :: Coterm v -> Env v -> Val v -> Result v Source #

lookupEnv :: Int -> Env v -> Val v Source #

Polynomial view

class PolyVal (t :: Ty) where Source #

Convert between the runtime Val representation and the polynomial Eval representation for a closed SysL type.

Methods

valToEval :: Val v -> Eval (SysLTy t) v Source #

evalToVal :: Eval (SysLTy t) v -> Val v Source #

Instances

Instances details

PolyVal 'One Source #
Instance details Defined in SysL Methods valToEval :: Val v -> Eval (SysLTy 'One) v Source # evalToVal :: Eval (SysLTy 'One) v -> Val v Source #
PolyVal 'Zero Source #
Instance details Defined in SysL Methods valToEval :: Val v -> Eval (SysLTy 'Zero) v Source # evalToVal :: Eval (SysLTy 'Zero) v -> Val v Source #
(PolyVal a, PolyVal b) => PolyVal ('Plus a b) Source #
Instance details Defined in SysL Methods valToEval :: Val v -> Eval (SysLTy ('Plus a b)) v Source # evalToVal :: Eval (SysLTy ('Plus a b)) v -> Val v Source #
(PolyVal a, PolyVal b) => PolyVal ('Times a b) Source #
Instance details Defined in SysL Methods valToEval :: Val v -> Eval (SysLTy ('Times a b)) v Source # evalToVal :: Eval (SysLTy ('Times a b)) v -> Val v Source #

SMC SMC compiler

type SMCThese = SMC (,) (->) Source #

Type synonym for the free symmetric monoidal target.

SMC (->) is the free SMC over plain functions. Boundaries are still expressed with These at the value level, but the free category itself uses the cartesian (,) tensor for SMCPar wiring rather than the inclusive These tensor. This avoids the impossibility of a Traced instance for These.

commandToSMC :: Command v -> SMCThese (Env v) (Result v) Source #

termToSMC :: Term v -> SMCThese (Env v) (These (Output v) (Val v)) Source #

cotermToSMC :: Coterm v -> SMCThese (Env v, Val v) (Result v) Source #

Process interpreter

evalProcess :: Term v -> Process (Env v) (Val v) Source #

Streaming interpreter: each input is a fresh environment, each output is the focus value of the term. Residual escape is a run-time error, which is the expected behaviour for a closed term consumed by a process.

Then as optic

thenLens :: (Val v -> Val v) -> (Val v -> Val v -> Val v) -> Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v)) Source #

Build a Then-style lens from explicit forward and backward maps.

The forward map a -> b and backward map a -> b -> a form a dependent lens Mono a a -> Mono b b in Poly.

applyThen :: Morphism (Mono (Val v) (Val v)) (Mono (Val v) (Val v)) -> Val v -> (Val v, Val v -> Val v) Source #

Apply a Then lens to an input value, returning the forward output and the backward continuation.

Regression tests

testId :: Result () Source #

Identity via Hom: (x -> x) VUnit.

testThen :: Result Double Source #

Thread a Double through Then.

testIdLoop :: Result () Source #

Identity test compiled to SMC.

testThenLoop :: Result Double Source #

Then test compiled to SMC.