[Haskell-cafe] Object Oriented programming for Functional Programmers

[Timon Gehr]

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.
>