🚀 go-pugleaf

In article <6143@crdgw1.crd.ge.com> chao@sunflower.crd.ge.com (William Chao) writes:
>In the paper "Basic Polymorphic typechecking," by Luca Cardelli,
>Science of Computer Programming 8 (1987) pp. 147-172. On page 150:
>-----------------------------------------------------------------------
>Polymorphism in language comes from the interaction of two contrasting
>programming language design goals: static typing and reusability.
>             :
>             :
>Polymorphic type systems try to reconcile these two goals
>by providing all the safety of statically typed languages,
>and most (but not all) the flexibility of untyped languages.
>-----------------------------------------------------------------------
>My 1st question: Why he says "but not all?"

Because there is a theoretical limit to the amount of type-checking that
is automatable.  To check, at compile time, that a program written in
(say) Lisp is well typed you need basically to verify the program, and
that is undecideable.

You could think of the amount of type checking that is possible as
analogous to (decidable) propositonal calculus, while to get the sort of
type checking you would like in Lisp, you need something analogous to
(undecidable) predicate calculus. 

>2nd question: It seems that the "full" flexibility of untyped languages
>              will never be achieved by static typing, then static binding.
>	      Does this imply that we got to have dynamic binding to accomplish
>	      the full reusability?

This is not really true, but you would need to bolt a theorem prover
onto the side of your compiler (see above).

>3rd question: [no answer here due to incompetence]

Sean