exotic type systems: linear types

[Mark Tarver]

Linear types corresponds to linear logic and ensures that objects are used exactly once, allowing the system to safely deallocate an object after its use.

Neal wrote to me about this.  Can we do linear types in Shen?  Generally it is easy to add to Shen, but sometimes you need to remove features if what you want to do is inconsistent from the underlying system.  Shen gives (enable-type-theory -)  for Shenturians who want to experiment like this.  Linear logic is different enough to warrant seeing how to do this.

 We use Shen sequent calculus to rebuild the type system from scratch. The key is that we keep control of the hypothesis list ourselves and we avoid branching in our type proofs by keeping the problems on our own stack.

Let's first see how this works for the non-linear case.  Here is the program in sequent calculus.

 (datatype nonlinear

____________________________

  (enable-type-theory +) : boolean;   \\ so we can back to reality!!

 

  \\ this rule just grabs the type problem from the 

  \\ checker and sends it to our system placing the problem 

  \\ and the type onto stacks 

   !; (() (X) (A));  

   ________________

   X : A; 

  \\ if the stack of problems is empty we're done;

   _________________  

   (_ () _);

 

   \\  solve by hypothesis

   (member (P A) Hyps);  

   (Hyps Rest B);

   ____________________________

   (Hyps (P | Rest) (A | B));

   

   ___________________

   (member X (X | _));

   

   (member X Hyps);

   _____________________

   (member X (_ | Hyps));

   

   \\ solve N : number if N is a number

   if (number? N)  

   (Hyps Rest B);

   _______________________________

   (Hyps (N | Rest) (number | B));

   

   \\ solve using the type of + 

   (Hyps Rest B);  

   _____________________________________________

   (Hyps (+ | Rest) ((number --> (number --> number)) | B));

   

   \\ solve if an application

   (Hyps (F X | Y) ((A --> B) A | C));  

   ________________________________________

   (Hyps ((F X) | Y) (B | C));)

Let's give this a go.

(1+) (enable-type-theory -)

false : boolean

(2+) (+ 6)

#<CLOSURE (LAMBDA (V2081)) {100451DC4B}> : (number --> number)

(3+) (+ 6 7)

13 : number

(4+) (* 6 7)

type error 

Weird.  Let's get into our old reality.

(5+) (enable-type-theory +)

true : boolean

(6+) (* 6 7)

42 : number 

Now let's try a linear type theory in which assumptions are bounded resources and can only be used once.

   

(datatype linear

 

  ____________________________

  (enable-type-theory +) : boolean;   \\ so we can back to reality!!

  \\ this version adds a hypothesis about *

   !; (((* (number --> (number --> number)))) (X) (A));

   ________

   X : A;

 

   _________________

   (_ () _);

 

\\ hypotheses are removed when used

   (remove (P A) Hyps NewHyps);

   !;

   (NewHyps Rest B);

   ____________________________

   (Hyps (P | Rest) (A | B));

   

   ___________________

   (remove X (X | Hyps) Hyps);

   

   (remove X Hyps NewHyps);

   _____________________

   (remove X (Hyp | Hyps) (Hyp | NewHyps));

   

   if (number? N)

   (Hyps Rest B);

   _______________________________

   (Hyps (N | Rest) (number | B));

   

   (Hyps Rest B);

   _____________________________________________

   (Hyps (+ | Rest) ((number --> (number --> number)) | B));

   

   (Hyps (F X | Y) ((A --> B) A | C));

   ________________________________________

   (Hyps ((F X) | Y) (B | C));)    

Let's give it a whirl.

(9+) (preclude [nonlinear])

[type#linear] : (list symbol)

(10+) !1

(enable-type-theory -)

false : boolean

(11+) (* 6 7)

42 : number

(12+) (* 6 (* 7 8))

type error

This fails because we tried to use the same hypothesis twice.  Really weird- time to exit this linear reality!

(13+) (enable-type-theory +)

true

(14+) (preclude [linear])

[] : (list symbol)

and we're back.  

Mark

       

[Neal Alexander]

This is quite a nice feature, since the core shen language is so minimal it could be built outward in radically different directions.

For example, you could disallow mutation and general recursion and create a strong/total functional language similar to Charity (http://pll.cpsc.ucalgary.ca/charity1/www/home.html).  

Since these features are a restricted subset, code written for this new language would be reusable in normal shen.

[Neal Alexander]

Can't linear types be done using a mutable vector as a dependently typed portion of the element's type signature? The type checker would then mutate this vector to de-activate the type after it has been consumed once and apply prolog cuts at the right places to prevent backtracking. Update operations would create a fresh vector to wrap its result. 

Below is a sample implementation, which superficially seems to work, but I don't know enough about T* to be sure. The cuts are maybe not correct either.

(tc -)

(define linear.discard

  [linear X] -> X)

(define linear.update

  F [linear X] -> [linear (F X)])

(tc +)

(datatype linear

              let T (@v true <>)

                    X : A;

         =============================

          [linear X] : (linear T A);

               if (<-vector T 1)

                      !;

             ____________________

              (linear.valid? T);

        let Unused (vector-> T 1 false)

                      !;

          ___________________________

            (linear.invalidate T);

               X : (linear T A);

              (linear.valid? T);

            (linear.invalidate T);

          __________________________

            (linear.discard X) : A;

              let T2 (@v true <>)

               X : (linear T A);

                F : (A --> A);

              (linear.valid? T);

            (linear.invalidate T);

    _______________________________________

      (linear.update F X) : (linear T2 A);

                       )

\\ ok

(let L  [linear 1]

     L2 (linear.update (+ 1) L)

   (linear.discard L2))

\\ type error

(let L  [linear 1]

     L2 (linear.update (+ 1) L)

   (linear.discard L))

[Raoul Duke]

btw minor thing perhaps worth keeping in mind is that linear types !== uniqueness types.

i know wikipedia can be wrong, but,

en.m.wikipedia.org/wiki/Substructural_type_system

:-)

[Mark Tarver]

You probably don't want to go down this path.  If you do, you'll be left with the management of these vectors if the proof backtracks and resources need to be freed up.  Shen Prolog

maintains such a vector itself and does the bookkeeping, so you're better off riding on that.

Associate a resource-bounded assumption with a variable Flag.  It can be used provided the variable is not set to used. When it is so, it acquires used as a value.

if (not (= Flag used))

(Flag ~ used);

_______________

(P Flag) >> P;

Mark

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, send an email to qilang+un...@googlegroups.com.
To post to this group, send email to qil...@googlegroups.com.
Visit this group at https://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.

[Neal Alexander]

Below is an updated version including Raould and Mark's comments. It is intended to be evaluated interactively. The goal is to be able to use different substructural typing behaviors cooperatively with regular Shen code via wrapper types.

For brevity I left out the definition of lambda, and reused the affine type instead of declaring a linear type. The linear behavior is being enforced via nested let statements, so the assumptions can be inspected for unconsumed types after the let body has been typechecked.

Are specially typed versions of let, lambda, and apply all that is really needed to enforce things? Since apply is the only way to unpack affine values, is that good enough?

What else needs to be done to make this practical? let/linear isn't a function and can't be implemented with Shen's single phase macro system. It can be done with a 3 phase macro system (which I have already been using for other things), but is there a simpler way?

(tc +)

(datatype marking

      ______________________

             (X ~ X);

         if (= Flag used)

    __________________________

        (consumed? Flag);

      if (not (= Flag used))

          (Flag ~ used);

    __________________________

        (consume Flag); )

(specialise $$)

(datatype affine

                          X : A;

             ________________________________

                [affine X] : (affine T A);

                    X : (affine T A);

                      F : (A --> B);

                       (consume T);

         _______________________________________

                     ($$ F X) : B; )

\\ ok: used once

(let X [affine 1]

   ($$ (+ 1) X))

\\ error: used twice

(let X [affine 1]

     A ($$ (+ 1) X)

   ($$ (+ 1) X))

\\ ok: never used

(let X [affine 1]

   10)

\\\\ linear

(specialise let/linear)

(datatype let/linear

                    if (variable? Var)

                  Expr : (affine T0 A);

                      (consume T0);

       Var : (affine T1 A) >> Body : (affine T2 B);

          Var : (affine T1 A) >> (consumed? T1);

    __________________________________________________

      (let/linear Var Expr Body) : (affine T2 B); )

(datatype test-functions

             _______________________________________________________

                     test : (number --> (affine T number));

    _________________________________________________________________________

             test2 : (number --> (number --> (affine U number))); )

\\ error: X is consumed twice

(let/linear X [affine 0]

  ($$ ($$ test2 X) X))

\\ error: Y is not consumed

(let/linear X [affine 0]

  (let/linear Y [affine 10]

    ($$ test X)))

\\ ok: X is consumed once

(let/linear X [affine 10]

  ($$ test X))

\\ ok: both X and Y are consumed

(let/linear X [affine 0]

  (let/linear Y [affine 10]

    ($$ ($$ test2 X) Y)))

\\ error: X is not consumed

(let/linear X [affine 0]

  X)

[Mark Tarver]

Bit complicated; try.

(0-) (datatype linear

______________

(X ~ X);

if (not (= Flag used))

(Flag ~ used);

___________________________

(linear X A Flag) >> X : A;

Y : B;

(linear X B Flag) >> Z : A;

_______________________

(let X (linearise Y) Z) : A;)

type#linear

(1-) (define linearise

          X -> X)

linearise

(2+) (let X (linearise 3)

             Y (* X 4)

            (+ X X))

type error   \\ the type of X is accessed twice

(3+) (let X (linearise 3)

              Y (* X 4)

              Y)

12 : number \\ only once is good

Mark

[Neal Alexander]

Hmm, I can't figure out why the return result is symbol:

(9+) (let X (linearise 1) X)

1 : symbol

[Mark Tarver]

You need to use placeholders and beta reduction to handle local assignments. Try the following.

Mark

(datatype linear

______________

(X ~ X);

if (not (= Flag used))

(Flag ~ used);

___________________________

(linear X A Flag) >> X : A;

let V (gensym &&)

let ZV/X (subst V X Z)  \\ cheapo beta reduction

Y : B;

(linear V B Flag) >> ZV/X : A;

_______________________

(let X (linearise Y) Z) : A;)

[Neal Alexander]

Well things are moving along nicely.

How to type linear 'if' seems like kind of a challenge though, since the state of linear variables in the first branch should not effect type checking of the second branch.

So you can either fork the assumption context somehow; or unify the type for one of the branches, then store the result in a mutable variable, then fail and bracktrack using the result to match against the type of the second branch. 

I'm not sure the second way would work though - doesn't it trim the search space? 

Is there a way to manipulate the assumption list directly?

[Neal Alexander]

Actually, I guess you don't need access to the whole assumption  list, since you can fork each element on a case by case basis.

             (fork Left Right);

          (left (linear X T Left)),

        (right (linear X T Right)),

                   >> P;

    __________________________________

     (linear X T Left) >> (branch P);

           if (= Flag used)

    _______________________________

           (fork Flag used);

        if (not (= Flag used))

    _______________________________

           (fork Flag New);

Gives:

1. (left (linear var2 string Var82))

2. (right (linear var2 string Var65))

3. (left (linear var1 number Var55))

4. (right (linear var1 number Var50))

from:

     (linear var1 number Flag), (linear var2 string Flag2) >> (branch P);

So it should be enough to replace the left/right tags with a branch unique id for pattern matching I guess.