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?

1. this only works with "dependent types", which Haskell does not have - by design (type inference/checking would be undecidable). It works in Coq, PVS etc. but there the programmer has to help the type checker (i.e. attach a proof that the type is correct) 2. using "type" (instead of "data") is generally a bad idea. J.W.

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