Re: [very] basic question

"Robert L. Constable" <rc@CS.Cornell.EDU> writes:


> Basically, the members of types are structured data elements, and the
> type describes the structure, telling how the elements are constructed.

this does not go along with many programming languages. In haskell the type of
1 is (Num a => a) which doesn't describe the structure, but what you can *do*
with it.

Nowadays, types are more and more used to tell what-you-can-do, than
what-is-the-structure of a value is. The what-you-can-do philosophy includes
the what-is-the-structure (since the what-you-can-do for basic types are given
as the minimal functions).

what-you-can-do doesn't have any implicit subtyping rules, whereas
what-is-the-structure do have implicit subtyping rules. But again many
languages do not use implicit subtyping (strutural equivalence), prefering
explicit/declared subtyping (declaration equivalence)

The result is that there is no more any simple mapping from values to types.
Values are tagged into types.

If you dissociate values from types, you can still see types as sets, but only
for supertyping:

  true = True
  false = False
  bool supertype of true and false
  => bool = True \/ False
  and define the order relation as (classical subsetting)
    True < True \/ False

  vehicle = Vehicle
  car subtype of vehicle
  => car = Vehicle /\ Car_
  and define the order relation as (inverse of subsetting)
    Vehicle > Vehicle /\ Car_

- solution1 nicely models extensible variants
- solution2 nicely models the OO subtyping
- so most languages do not follow any subsetting relation since most languages
allow subtyping, but not supertyping.
- true, false, bool are variables
- True, False, Vehicle, Car_ are simple type constants
- the subtyping relation is strictly structural
  - every normalised types is a union of intersection of basic types
  - basic types are all unrelied: we have neither C1 subtype of C2 or C2
    subtype of C1
  - the subtyping relation is defined only on /\ and \/
  - normalisation of types is simple (see normalisation of functions below)
- Car_ alone is not a legal type, but it won't appear alone in type
- programming languages usually do not allow mixing types, in that case 
an expression can't have type "True /\ Vehicle" or "True \/ Vehicle"


> A key practical difference is that functions in the type A->B are
> polymorphic whereas those in the set of functions from A to B are not.
> This makes subtypes behave differently than subsets, so for example if
> A[A' (A is a proper subtype of A') and B[B', then (A'->B)[(A->B'),
> i.e. subtyping is co-variant on the domain.  This basic difference
> shows up in the definition of records for example.

the contravariance on parameters and covariance on result is a property of "->" :

true -> false  defined as   True -> False
bool -> false  defined as   True -> False /\ False -> False
true -> bool   defined as   True -> True  \/ True  -> False
bool -> bool   defined as   (True -> True /\ False -> True) \/ 
                            (True -> False /\ False -> False)
and we do have
  bool -> true  <  true -> true  <  true -> bool

vehicle -> vehicle   defined as   Vehicle -> Vehicle
vehicle -> car       defined as   Vehicle -> Vehicle /\ Vehicle -> Car_
car     -> vehicle   defined as   Vehicle -> Vehicle \/ Car_ -> Vehicle
car     -> car       defined as   (Vehicle -> Vehicle /\ Vehicle -> Car_) \/ 
                                  (Car_ -> Vehicle /\ Car_ -> Car_)
and we do have
  vehicle -> car <  vehicle -> vehicle  <  car -> vehicle

* ad'hoc overloaded functions can be typed:
  a function over Int returning Int, and also over String returning String
    (Int -> Int) /\ (String -> String)
  this type is compatible with:
    (Int -> Int) /\ (String -> String)  <  (Int -> Int)
    (Int -> Int) /\ (String -> String)  <  (String -> String)

(some more at http://merd.net/pixel/language-study/types.txt)

programming languages addict      http://merd.net/pixel/language-study/