[merd-devel] typing

[Pixel <pi...@ma...>]

Ok, now what's a ``type''? I had some pb defining it in the language and had to
think about it. Here is the result...

def: a "type" is a "set of values"


1. Simple type system with static-typing


Without subtyping, you have a set of types having a set of values:
{
  byte => { 0, 1, ..., 255 },
  bool => { true, false },
  char => { 'a', 'b', ... },
  string => { "", "a", ... },
  list(byte) => { [], [0], ... },
  ...
}

What is the use of types in a static typed language like java?

1.1. storing the values
Knowing the range of values permits nice storage:
- for a "2 value" type, 1 bit is enough to know which value it is (eg: booleans)
- even for "infite set of values" type, you can at least assume things about the
values (eg: strings are build with caracters)

1.2. ensuring ``correctness''
That is, ensure "strong typing", meaning you don't misinterpret a value of being
type "a" whereas it is type "b". This 

This *must* be done at compile-time, otherwise you loose feature 1.1.


1.3. having a function with different semantic based on types
overloading and polymorphism ad'hoc

eg: based on the type ``+'' behaves differently (addition (numbers),
concatenation (strings, lists))



2. Dynamic typing

Let's see if the previous points still hold:


2.1. storing the values
Types have always been used to store values. In dynamically types languages,
this is not really true anymore. The language must be prepared to accept every
values.

2.2. ensuring ``correctness''
Not needed at compile-time, easily done at run-time

2.3. overloading
For this one, you need to specify types, otherwise the interpreter can't know
for which type you're defining the function. Solved in object oriented language
by defining a class for which the functions (methods) are defined.


3. Dynamic/static typing comparison

In both cases, the interpreter verifies that the types match. Either this check
is done at compile-time or run-time. At run-time, you know the value so the
type. At compile-time, you don't know the value but you know the type.

Based on this, one can say that the types purpose is to have a compile-time set
of the values a variable can take.
(one could define types that can't be checked at compile-time?)


4. Enhancing ML: types as first-class citizen

In the following i'll try to unify ``types'' and ``values''
Let's allow:

let typ = string
typ : type

4.1. Benefits

- reflexivity: types can be used in lists, keys in hashes...
you can have typeof: a -> type

- type constructors:
let flistT a = (list of a) -> (list of a)
 (from a lambda-prolog example which was using a #define)

- clean: don't bother with values AND types, it is the same

4.2. Problems

- to keep static typing, the compiler must know every "type" value at compile
time. To do so the compiler must be able to interpret some code while infering
type, eg:

let t = flistT(flistT(int)) in
let (f : t) = ...

- overkill?



5. Subtyping and types

to come...