[Haskell-cafe] Object Oriented programming for Functional Programmers
Timon Gehr
timon.gehr at gmx.ch
Thu Jan 3 23:02:33 CET 2013
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.
>
More information about the Haskell-Cafe
mailing list