Some novel features of Scryer Shen
This article motivates and explains several of the novel features of Scryer Shen by illustrating their use in an advanced type theory.
If you’ve programmed in other Lisps you’ve probably come across the apply function. apply calls its first argument, a function, on the sequence of arguments supplied by its second argument, a heterogeneously typed list. Some examples of how our apply should work in Shen are
(1+) (apply + [1 2])
3 : number
(2+) (apply cons? [[1 a]])
true : boolean
(3+) (apply vector-> [(@v 1 2 <>) 2 3])
<1 3> : (vector number)The difficulty of implementing a type-safe apply in Shen is partly that Shen has no in-built concept of variadic functions at the type level. At first glance this doesn’t appear to be true; one can enter (+ 1 2 3 4 5) at the REPL and get back 15 : number when type checking is turned on. But this is something of an illusion: that the form (+ 1 2 3 4 5) type checks in Shen with no extraneous type theory defined is because a reader macro expands it to (+ 1 (+ 2 (+ 3 (+ 4 5)))) which is then submitted to the type checker.
What apply needs is a variadic function type whose number of arguments is constrained to match the number of elements of its second argument, a (heterogeneous) list. Can we come up with a type-level syntax for variadic functions satisfying this constraint?
The answer is yes, but it seems we have to extend the type system to do it. I tried to the best of my ability to implement the type theory I’m about to give in other Shen implementations, which lack the special Scryer Shen features used here, of course, and I could not make it type check. I encourage others in the Shen community to try!
We begin by introducing the concept of a heterogeneous list or h-list. We start with the most straightforward inductive definition valid in any Shen implementation:
(datatype heterogeneous-lists
_________________
[] : (h-list []);
X : T;
Xs : (h-list Ts);
=========================
[X|Xs] : (h-list [T|Ts]);)At first this seems perfectly fine. All information about the types of the elements making up the h-list are retained as a list in the h-list type in ordered one-to-one correspondence with the types of the value elements. We’ll soon run into a problem defining the apply function however.
Next we introduce the concept of h-mappable, or heterogeneously mappable, function. A function F : (h-mappable L R) is applicable to the values of type (h-list L) yielding a value of type R. By varying its L and R parameters, the h-mappable type family captures the entire family of Shen function types (albeit non-isomorphically thanks to currying). Any Shen function can be typed this way, so h-mappable is one manifestation of our sought variadic function type.
Suppose we want to prove that (fn +) : (h-mappable [T|Ts] R) for some argument types [T|Ts] and result type R, where the type variables T, Ts, and R are yet to be instantiated. Starting from the naive type theory
(datatype heterogeneously-mappable-functions
F : (--> R);
======================
F : (h-mappable [] R);
F : (T --> R);
=======================
F : (h-mappable [T] R);
F : (T1 --> (h-mappable [T2|Ts] R));
===================================
F : (h-mappable [T1 T2|Ts] R);our type theory so far is all in standard Shen.
Again, we must keep in mind that Shen functions are implicitly curried, seen from the fact that (fn +) has type (number –> (number –> number)) (the inner parens are not just for show!). From this, we’d like the type checker to infer that (fn +) : (h-mappable [number number] number).
We see that the third rule proves (fn +) : (h-mappable [number number] number) from the postulate (fn +) : (number –> (h-mappable [number] number)). Taking advantage of currying, the strategy is to step inductively through the argument types of F. The conclusion is the only inference whose form unifies to the starting hypothesis on (fn +), which is to say it’s the type checker’s only option.
Unfortunately it reaches an impasse there. The type checker has no way of progressing to the desired conclusion as there is nothing in the syntactic environment suggesting a path to it from its current (and only possible) position. All information about h-mappable comes from the heterogeneously-mappable-functions datatype, none of whose conclusions unify to (T1 –> (h-mappable [T2|Ts] R)).
To get around this we add a fourth rule to the type theory, which is now
(datatype heterogeneously-mappable-functions
F : (--> R);
======================
F : (h-mappable [] R);
F : (T --> R);
=======================
F : (h-mappable [T] R);
F : (T1 --> (h-mappable [T2|Ts] R));
===================================
F : (h-mappable [T1 T2|Ts] R);
F : (A --> B);
(h-list-to-function-sig [T|Ts] (A --> B) R);
____________________________________________
F : (h-mappable [T|Ts] R);)The fourth rule uses the Shen Prolog predicate h-list-to-function-sig to relate the function type (A –> B) to the list of arguments [T|Ts] and result type R. Importantly, h-list-to-function-sig goal is only executed after the value F is inferred to have the function type (A –> B).
The definition of h-list-to-function-sig is
(defprolog h-list-to-function-sig
[] R R <--;
[T1 T2|Ts] -->(T1 Rs) R <-- (h-list-to-function-sig [T2|Ts] Rs R);
[T] -->(T R) R <--;)Some examples of its use are
(0-) (prolog? (h-list-to-function-sig [T|Ts] -->(number -->(number number)) R)
(return [[T|Ts] R]))
[[number number] number]
(1-) (prolog? (h-list-to-function-sig [number number] -->(A B) number)
(return -->(A B)))
[--> number [--> number number]]We’ve already departed from standard Shen here in that a plain Shen Prolog predicate is being called from an inference rule in a datatype definition.
The apply function is
(define apply
{ (h-mappable [T|Ts] R) --> (h-list [T|Ts]) --> R }
F [X] -> (F X)
F [X1 X2|Xs] -> (apply (F X1) [X2|Xs]))We can see from its type that apply requires a non-empty list of arguments for F. What’s more, the sequence of argument types F takes is exactly that of the h-list in the second argument, meeting our first constraint.
It does not type check in its current form:
(4+) (define apply
{ (h-mappable [T|Ts] R) --> (h-list [T|Ts]) --> R }
F [X] -> (F X)
F [X1 X2|Xs] -> (apply (F X1) [X2|Xs]))
type errorWe can see where the failure occurs in the debugging window.
The first rule fails to type check (in [false, false] at the cursor, the first false is the sole relevant value indicating success or failure).
By wrapping calls in type-checker.pl with the $ meta-predicate from Scryer Prolog’s debug library and attempting the type check again in a fresh Scryer Shen instance, proof search calls are printed in the Debugging Window, shedding some light onto what went wrong.
It turns out that none of the hypotheses in the first three (double-sided) rules apply. In the first rule of apply, F : (h-mappable [T|Ts] R) is true by hypothesis. The problem is that nothing further can be inferred under the present type theory!
If the type checker could equate Ts to [], which should make intuitive sense to we humans, the second rule of heterogeneously-mappable-functions would apply.
This is not a valid inference in the sight of the type checker or in standard Shen type theory, for the following reason. To the outside world, T and Ts are universally quantified type-level variables whose values may vary across call sites according to the ever changing type of F. Therefore, in the context of proving that (F X) : R, T and Ts must not be allowed to unify to more specific values since proof search would then be logically unsound.
Standard Shen implementations enforce this constraint using mode declarations (more or less, by refraining from fully general unification in hypothetical contexts and preferring “read only” pattern matching instead). Scryer Prolog does not have mode declarations but does support attributed variables in the tradition of SICStus Prolog. Attributed variables are used in the Scryer Shen type checker to insert hooks on suitably tagged (one might say attributed) variables invoked at unification to prevent logically unsound specifications from occurring.
The good news is that this prohibition can be conditionally circumvented by overriding the verify_attributes/3 predicate. Leveraging this, Scryer Shen allows the Shen programmer to define exceptions to this rule under their own type theory. Our heterogeneous-lists datatype thereby becomes
(datatype heterogeneous-lists
____________________________
[] : (h-list Ts) >> Ts ~ [];
_______________________________________________________________
[X|Xs] : (h-list Ts) >> X : T, Xs : (h-list Tss), Ts ~ [T|Tss];
_________________
[] : (h-list []);
X : T;
Xs : (h-list Ts);
_________________________
[X|Xs] : (h-list [T|Ts]);)The top two rules are new and both use the ~ or type equality operator. The first rule states that given the hypothesis [] : (h-list Ts), Ts can be equated to []. The second similarly allows Ts to be expanded to [T|Tss] where T and Tss are existential types in the new hypotheses X : T and Xs : (h-list Tss) where [X|Xs] : (h-list Ts).
Once these equations are made, T and Tss are again “frozen” according to the above convention for hypothetical type variables but may of course be unfrozen again by future type equality inferences.
We now summarize all we’ve done in a final Shen session culminating in the example evaluations we first set out to realize.
(0-) (tc +)
(1+) (datatype heterogeneous-lists
____________________________
[] : (h-list Ts) >> Ts ~ [];
_______________________________________________________________
[X|Xs] : (h-list Ts) >> X : T, Xs : (h-list Tss), Ts ~ [T|Tss];
_________________
[] : (h-list []);
X : T;
Xs : (h-list Ts);
_________________________
[X|Xs] : (h-list [T|Ts]);)
(2+) (defprolog h-list-to-function-sig
[] R R <--;
[T1 T2|Ts] -->(T1 Rs) R <-- (h-list-to-function-sig [T2|Ts] Rs R);
[T] -->(T R) R <--;)
(3+) (datatype heterogeneously-mappable-functions
F : (--> R);
======================
F : (h-mappable [] R);
F : (T --> R);
=======================
F : (h-mappable [T] R);
F : (T1 --> (h-mappable [T2|Ts] R));
====================================
F : (h-mappable [T1 T2|Ts] R);
F : (A --> B);
(h-list-to-function-sig [T|Ts] (A --> B) R);
____________________________________________
F : (h-mappable [T|Ts] R);)
(4+) (define apply
{ (h-mappable [T|Ts] R) --> (h-list [T|Ts]) --> R }
F [X] -> (F X)
F [X1 X2|Xs] -> (apply (F X1) [X2|Xs]))
apply : ((h-mappable [A | B] C) --> ((h-list [A | B]) --> C))
(5+) (apply + [1 2])
3 : number
(6+) (apply + [1 2 3])
type error \* this is expected: + takes up to 2 arguments *\
(7+) (apply cons? [[1 a]])
true : boolean
(8+) (apply vector-> [(@v 1 2 <>) 2 3])
<1 3> : (vector number)apply works for partial applications as well:
(9+) (apply + [1]) curried:+ : (number --> number) (10+) (apply +) curried:apply : ((h-list [number]) --> (number --> number))
If we wanted to bring the (h-mappable [T|Ts] R) <–> (T –> … –> R) mapping closer to an isomorphic correspondence, we could use the dif/2 constraint provided by Scryer Prolog’s dif library. dif/2 provides declarative disequality between Prolog terms, allowing inequality between select terms to be enforced without giving up the logical purity of the resulting Prolog predicates.
After loading the library in Scryer Prolog, the modified heterogeneously-mappable-functions datatype is
(12+) (prolog? (use-module (library dif)))
true
(13+) (datatype heterogeneously-mappable-functions
F : (--> R);
======================
F : (h-mappable [] R);
(dif R -->(_ _));
F : (T --> R);
=======================
F : (h-mappable [T] R);
(dif R -->(_ _));
F : (T1 --> (h-mappable [T2|Ts] R));
===================================
F : (h-mappable [T1 T2|Ts] R);
F : (A --> B);
(h-list-to-function-sig [T|Ts] (A --> B) R);
____________________________________________
F : (h-mappable [T|Ts] R);)
heterogeneously-mappable-functions#typeThe dif goals limit the occurrence of F’s argument types to [T|Ts] and do so in either mode of the double-sided rules.
It is also worth noting how these changes take advantage of Scryer Shen’s support for arbitrary Prolog functors. Specifically the Prolog functor (–>)/2 is used to prevent result types R from being unified to function types with at least one argument.
A truly general apply, one that will “apply” argless functions in the manner of other apply boasting Lisps, is
(define apply
{ (h-mappable Ts R) --> (h-list Ts) --> R }
F [] -> (F)
F [X] -> (F X)
F [X1 X2|Xs] -> (apply (F X1) [X2|Xs]))Note that the previous definition did not need an empty h-list case since the type (h-list [T|Ts]) only admits non-empty lists. For that reason, the previous apply could only apply functions of arity 1 and above.
The final (and, I think, rather beautiful and elegant) Shen program can be found here. There the original apply is renamed as apply1.