🚀 go-pugleaf

i though i posted a note yesterday but it failed to appear,
so i'll try try again.


>fs@caesar.cs.tulane.edu (Frank Silbermann) writes:

>C) I've never seen a programming language
>   based on typed lambda calculus whose typechecking system
>   permits the user to define a fixpoint combinator
>   out of more primitive elements.  The type signature
>   of the necessary lambda expression cannot be written
>   as a finite combination of the primitive types
>   (so Y-combinators must be added as primitives).

if one adds ml references to the simply typed (lazy) lambda calculus,
then for each non-empty  functional type (s->t) one can write 
a fixpoint combinator for that type. assume that g: s-> t, then
(using a mish mash of typed lambda calculus and ml notation) one
such example is

 lambda N : (s->t)->(s->t) . 
    let z = ref g in  ( z := (lambda x : s . ( N(! z)(x))) ; (! z)

note that g is only used as a dummy to allocate the necessary cell
for the  self reference.

		-iam-