🚀 go-pugleaf

>  I didn't have in mind any particular concept of strong typing, other than
>the idea that you have to be able to determine at compile-time what type
>things are. Sorry, but I'm not a type-theorist. My particular favourite is
>Milner polymorphism, because it's easy and it provides exactly the type
>information which an implementation needs and can use. That is, you need to
>know the information that Milner typing gives you, and you cannot take
>advantage of any more. Correct me if I'm wrong, please.
>
Why should type checking be restricted to compile time?
It is perfectly possible to have strong typing which is done wholely
at run-time (any interpreter is going to behave like that).
Currently most systems do some type checking at run time: what is a
divide-by-zero eroor trap except a type failure indication from the hardware?
If you believe that Milner-style type checking is adequate, would you be happy
to modify your hardware to not cause this trap but deliver some result of the
operation instead? 
Is "tail" defined on lists or on non-nil lists? If the latter, how do you cope
with this in a Milner-style system (pretty clumsily, if at all, I would guess).
 
Personally I would like the type system to ensure, when I reduce a function 
over a set, that that function is commutative and associative (since the
reduction operation is otherwise undefined).  I would also like it to check
that the unit used in the reduction has the right properties.  I can't imagine
doing this in a type system that doesn't allow me to make assertions that it is
unable to check (actually I can, but doing the operation 2**n times and making
sure all the results are the same is not what I want it to do); do Milner style
systems give this sort of information? I guess not, but I'm absolutely
certain you can take advvantage of it.
 
Tom Thomson  [tom @ me.stl.stc.co.uk
 
PS: No, I don't know any language implementations that let me do this,
    more's the pity.