Implementing dependent types in Turner and a note on T*

[Mark Tarver]

I turfed out my copy of Raymond Turner's "Constructive Foundations for Functional Languages" and turned to the section on dependent types.  In it he has an axiom DP. which is written thus

DP. f is a member of (pi x S T) <-> all x [x is a member of S -> [f x] is a member of T].

He remarks

"This generalizes the ordinary notion of a general function space which is a special case where x is not free in T."

In Shen its easier to understand:

(all X ((X : S) => ((F X) : T)));
===============================
F : (- (pi X S T));

To make this work you need rules for universal quantification

let Y (gensym t)
let PY/X (subst Y X P)
PY/X;
__________
(all X P);

let PY/X (subst Y X P)
PY/X >> Q;
_______________
(all X P) >> Q;

as well as rules for implication

P >> Q;
_________
(P => Q);

(P => Q) >> P;
_______________
(P => Q) >> Q;

To give it a whirl I tried this example.

(103+) (fn +) : (pi x number (number --> number))
____________________________________________________________ 6 inferences
?- (lambda Y9299 (lambda Y9300 ((+ Y9299) Y9300))) : (pi x number (number --> number))

>
____________________________________________________________ 15 inferences
?- (all x ((x : number) => (((lambda Y9299 (lambda Y9300 ((+ Y9299) Y9300))) x) : (number --> number))))

>
____________________________________________________________ 22 inferences
?- ((t9301 : number) => (((lambda Y9299 (lambda Y9300 ((+ Y9299) Y9300))) t9301) : (number --> number)))

>
____________________________________________________________ 30 inferences
?- ((lambda Y9299 (lambda Y9300 ((+ Y9299) Y9300))) t9301) : (number --> number)

1. t9301 : number

>
____________________________________________________________ 37 inferences
?- (lambda Y9299 (lambda Y9300 ((+ Y9299) Y9300))) : (Var5 --> (number --> number))

1. t9301 : number

>
____________________________________________________________ 43 inferences
?- (lambda Y9300 ((+ &&Y9299) Y9300)) : (number --> number)

1. &&Y9299 : Var5
2. t9301 : number

>
____________________________________________________________ 51 inferences
?- ((+ &&Y9299) &&Y9300) : number

1. &&Y9300 : number
2. &&Y9299 : Var5
3. t9301 : number

>
____________________________________________________________ 62 inferences
?- (+ &&Y9299) : (Var10 --> number)

1. &&Y9300 : number
2. &&Y9299 : Var5
3. t9301 : number

>
____________________________________________________________ 73 inferences
?- &&Y9299 : number

1. &&Y9300 : number
2. &&Y9299 : Var5
3. t9301 : number

>
____________________________________________________________ 80 inferences
?- &&Y9300 : number

1. &&Y9300 : number
2. &&Y9299 : number
3. t9301 : number

>
____________________________________________________________ 85 inferences
?- t9301 : number

1. t9301 : number

>
#<FUNCTION (LAMBDA (Y9299)) {1004553B9B}> : (pi x number (number --> number))

However if I enter this:

(define f
  {(pi x number (number --> number))}
   X Y -> (+ X Y))
   
I'll get an error.

The source of the error is T*.  T*, as you might know, is derived from T, and T* is a procedural abstraction from T that cuts out a lot of boilerplate reasoning.  The result is that T* is about 7X faster than T.  Back in the days of 166MHz processors, this meant a lot.  The reason that T can cut corners like this is that it makes certain assumptions about the types it is dealing with; principally, that they are conventional function space types.

Now two questions arise here.  First can this situation be changed without going all the way back to T? And second, should we bother?   To take the second question first, I'm sceptical about the utility because taking type theory much beyond T* really takes us into formal methods and for that there are other routes WMO are easier and better to follow (typed second order logic).  

However ....

To answer the first question; 'yes' it can be done.  And moreover it can be done without disturbing the proofs of soundness in TBoS.   To achieve this we convert a Shen rule P1 ...Pn -> R into the pattern matching abstraction (/. P1 ... (/. Pn R) ...) and then we implement the Patterns Rule. The rule is type checked just like a regular expression and as a plus we can add our pi rule and actually get Shen to attach this type to a function definition.   The price is that we have to admit pattern matching abstractions as first class objects.  We can call this approach T+.

But going back to Turner he failed to sell his fish by not providing a clear and motivating example for DP.  So I still remain from Missouri about this.  But can it be done in Shen with small modification?  

Yes.