[Prev][Next][Index][Thread]
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:
solution1:
true = True
false = False
bool supertype of true and false
=> bool = True \/ False
and define the order relation as (classical subsetting)
True < True \/ False
solution2:
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
expressions
- 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)
--
Pixel
programming languages addict http://merd.net/pixel/language-study/