[Haskell-cafe] Types in bounds

[Marc Weber]

On Mon, Sep 01, 2008 at 11:45:12AM +0200, Brettschneider, Matthias wrote:
>    Hey there,
> 
> 
> 
>    i was just thinking about types in Haskell and I asked myself,
> 
>    Is there a mechanism, that allows me to define a new type out of an
>    existing one with some restrictions?
> 
>    So that the new type is a subset of the existing one.
> 
> 
> 
>    Lets imagine I want a type for a point like:
> 
>    type Point = (Int, Int)
> 
>    But what, if I can predict that the X and Y values are in a range between
>    0 and 100?
> 
>    If someone defines a new point like:
> 
>                    p :: Point
> 
>                    p = (200, 400)
> 
>    that is totally fine with the type definition above, but not correct in my
>    context.
> 
> 
> 
>    Is it possible, to put this information into the type? So that the
>    compiler is able to recognize my mistake?

Sure, have look at the database library haskelldb (1)
It contains one module doing exactly this for Strings and it's length.
There are at least two packages on hackage dealing with type level
integers (eg the type-level library letting you use D1 :* D2 = 12)
This way you can statically check some things, however you won't be able
to statically assure that say
strangeNewPoint (a,b) (c,d) = (a*c,b-d) will be within the given range
as well without doing all the calculations in type level programming..
(But then you no longer need te program..)

(1) http://hackage.haskell.org/packages/archive/haskelldb/0.10/doc/html/Database-HaskellDB-BoundedString.html

But depending on your usage it may be the easiest apporach to live with
some runtime checks (see assert in the ghc manual)..

Sincerly
Marc Weber