Re: What is the Shen equivalent of "System F"

[Mark Tarver]

The equivalent to system F is here:

http://www.lambdassociates.org/Book/page267.htm

You can probably research the differences by comparison.

Mark

On Nov 25, 9:52 am, Artella Coding <artella.cod...@googlemail.com>
wrote:
> Hi, the Haskell compiler ghc desugars haskell code to an intermediate
> language called Core which is based on System FC (which is an extension of
> System F, a "typed lambda calculus" :http://en.wikipedia.org/wiki/System_F)
>
> What is the Shen equivalent to System F? And how different is it from
> System F?

[Mark Tarver]

In a rush but a few words of clarification.

The bedrock of most type theories is the simply typed lambda calculus
which is very basic and does not suffice for handling recursion.  So
most type theories augment that type theory by additional rules.  Shen
does it and so do other languages.  System F augments STLC by
universal quantification over types thus allowing polymorphism.  If
this quantification is restricted in certain ways then what you get is
a language in which type checking in decidable. In this sense system F
can be used as the basis for a language like Haskell.  At the far end
of the scale you have stuff like Martin-Lof which is undecidable.

Mark

[Mark Tarver]

One distinction between system F and Shen concerns the treatment of
quantified types.

For example suppose I want to define a function foo that takes a
higher-order function F of type A --> A and applies it thus:

(define foo
{(A --> A) --> (number * symbol)}
F -> (@p (F 1) (F a)))

We find that this fails. Shen treats the problem

Prove foo : (A --> A) --> (number * symbol)

meaning

For any type A, prove foo is of type (A --> A) --> (number * symbol)

meaning

Let &&A be some arbitrary type;
prove foo is of type (&&A --> &&A) --> (number * symbol).

This fails because Shen says

OK; assume F : (&&A --> &&A) I have to prove (@p (F 1) (F a)) :
(number * symbol). But I cannot prove (F 1) : number because F does
not have the right type.

What we are trying to express is not

For any type A, prove foo is of type (A --> A) --> (number * symbol)

but

Prove foo is of type ((forall A (A --> A)) --> (number * symbol))

This is known as a deep type as opposed to a shallow type. The
universal quantifier is embedded inside the type as opposed to outside
(prenex form). See bottom of
http://www.cmi.ac.in/~madhavan/courses/pl2009/lecturenotes/lecture-notes/node110.html

So you have:

(define foo
{(forall A (A --> A)) --> (number * symbol)}
F -> (@p (F 1) (F a)))

Hence Shen reasons

OK; assume F : (forall A (A --> A)) I have to prove (@p (F 1) (F a)) :
(number * symbol).

In order to discharge this proof you need rules for quantified types
allowing you to instantiate the bound variable. In system F you have
something a bit like this. You can program this into Shen by creating
a schema on demand and use unification and discharge the above.

(datatype qtypes

let C (subst (arbterm) A B)
X : C;
____________
X : (mode (forall A B) -);

(scheme A B D E);
X : D >> X : C;
_______________________
X : (mode (forall A B) -) >> X : C;

!;
_______________
(scheme A A E E);

!;
(scheme A B D F);
(scheme A C E F);
___________________________
(scheme A (B | C) (D | E) F);

______________
(scheme A B B C);)

(define arbterm
-> (gensym &&))

Mark