I have been thinking, again, about way’s in which one can encode linear variable usage in EDSLs.
One cannot state usage on things that one cannot bind.
We can encode EDSLs using intrinsically well-typed EDLS that, at the type-level, gives all terms a type
type and carries around the local typing context.
Bound variables are represented using De Bruijn indices encoded as existential quantification over a type-level context.
This traditional approach, however, does not play well with languages that have built in ways to ensure linear variable usage.
Take for example the follow example of the STLC in Idris2.
data Ty = TyBool | TyFunc Ty Ty namespace Orig data STLC : (ctxt : List Ty) -> (type : Ty) -> Type where Var : Elem type ctxt -> STLC ctxt type Func : (body : STLC (type_param :: ctxt) type_body) -> STLC ctxt (TyFunc type_param type_body) App : (func : STLC ctxt (TyFunc type_param type_body)) -> (param : STLC ctxt type_param) -> STLC ctxt type_body B : (b : Bool) -> STLC ctxt TyBool
If we want to turn this into the STLC in which variables are only used once then we need to restrict variable usage.
Quantitative Type-Theory is built into Idris2 and we can state such usage on binders as follows:
double : Num a => (1 x : a) -> a
Here the argument
double must be used once.
But how can we do this for
Bound things are De Bruijn indexed, and we do not have an explicit binder to state usage on in the EDSL definition itself.
Let’s fake it by explicitly tracking variable usage in the type.
A simple thought occurred to me is that if we are just thinking about linear variable usage then we can enhance the definition of
STLC to explicitly track variable usage.
We do so in four key ways:
- We change the context to associate each bound type with a usage
- We further paramterise
newcontexts that help us track how the context changes wrt to variable usage, and update our type-system accordingly
- We change the definition of our existential quantifier
Elemsuch that each proof updates the usage for the found bound variable
- We ensure that for functions the parameter passed in is used at most once.
Thus our previous EDSL now becomes
data Usage = USED | FREE data Item : Type where MkItem : Usage -> (ty : Ty) -> Item data HasItem : Item -> List Item -- Old -> List Item -- New -> Type where H : HasItem (MkItem FREE ty) (MkItem FREE ty :: rest) (MkItem USED ty :: rest) T : HasItem (MkItem FREE ty) rest rest' -> HasItem (MkItem FREE ty) (MkItem x ty' :: rest) (MkItem x ty' :: rest') data FakeLSTLC : List Item -- old -> List Item -- new -> Ty -> Type where Var : HasItem (MkItem FREE ty) old new -> FakeLSTLC old new ty Func : (body : FakeLSTLC (MkItem FREE paramTy :: old) (MkItem USED paramTy :: new) bodyTy) -> FakeLSTLC old new (TyFunc paramTy bodyTy) App : (func : FakeLSTLC old new (TyFunc paramTy bodyTy)) -> (param : FakeLSTLC new new' paramTy) -> FakeLSTLC old new' bodyTy And : FakeLSTLC old new TyBool -> FakeLSTLC new new' TyBool -> FakeLSTLC old new' TyBool B : Bool -> FakeLSTLC old old TyBool
HasItemdestroys and rebuilds the typing context
- In the definition of
Funcwe ensure that the parameter must be used
Appthreads the context changes through each term
Bdoesn’t alter the context as it is a pure value
and with this we can write examples:
example : FakeLSTLC Nil Nil TyBool example = App (Func (And (B True) (B True))) (B True)
1/1: Building 2021-01-25-Fakiing-Linear-Variables (2021-01-25-Fakiing-Linear-Variables.md) Error: While processing right hand side of example. When unifying FakeLSTLC (MkItem USED ?paramTy :: ?old) (MkItem USED ?paramTy :: ?old) TyBool and FakeLSTLC (MkItem FREE ?paramTy :: ?old) (MkItem USED ?paramTy :: ?old) TyBool. Mismatch between: USED and FREE. 2021-01-25-Fakiing-Linear-Variables.md:117:27--117:33 | 117 | example = App (Func (And (B True) (B True))) (B True) | ^^^^^^
the variable must be used, but is not. This example will pass:
example1 : FakeLSTLC Nil Nil TyBool example1 = App (Func (And (Var H) (B True))) (B True)
This next one will fail because of the duplicate variable usage:
example2 : FakeLSTLC Nil Nil TyBool example2 = App (Func (And (Var H) (Var H))) (B True)
Error: While processing right hand side of example2. When unifying FakeLSTLC (MkItem FREE TyBool :: ?new) (MkItem USED TyBool :: ?new) TyBool and FakeLSTLC (MkItem FREE TyBool :: ?old) (MkItem FREE TyBool :: ?new) TyBool. Mismatch between: USED and FREE. 2021-01-25-Fakiing-Linear-Variables.md:146:28--146:33 | 146 | example2 = App (Func (And (Var H) (Var H))) (B True) | ^^^^^