On 01/03/2013 10:56 AM, Alberto G. Corona wrote:
Anyway, Type checking is essentially an application of set theory : (I
did no search in te literature for this, It is just my perception).
Not exactly. Type theory is not an application of set theory, it is an
alternative to set theory.
When
I say (+) :: Num a => a -> a -> a . I mean that (+) takes two elements
of the set of Num typeclass and return another.
If I get this right, you consider Num to be a set, and then its
inhabitants would need to be be types, thus this describes a type-level
mapping.
This is a more accurate description, (but there might be a better one):
(+) : (a : Type)->(i : (Num a : Prop))->(x : a)->(y : a)->(z : a)
(+) is a mapping from types 'a' to mappings from proofs 'i' of the
proposition that 'a' is an instance of the 'Num' type class to a curried
function that takes two arguments of type 'a' and produces a result of
type 'a'.
This is in principle a
weak restriction, because many functions do it as well, for example (*).
A propery check or a contract would be much more restrictive and thus
would detect much more program errors. But it seems that no other
language but haskell took this set theoretical analysis so exhaustively,
There are quite a few that take it further than Haskell.
http://wiki.portal.chalmers.se/agda/pmwiki.php
and without it, a property check is like detecting microscopic cracks in
nuclear waste vessel without first making sure that the cover has been
sealed.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
