Creating a type for a subset of the integers

newer
Class/Instance : what am I doing...

older
Re: [Haskell-cafe] [HXT] Simple...

Brad Larsen

19 Dec 2007 19 Dec '07

2:07 a.m.

Hi there list, How would one go about creating a new type for a subset of the integers, for (contrived) example just the even integers? I was thinking of making a new type newtype EvenInt = EvenInt Integer but the problem with this is that it accepts any integer, even odd ones. So to prevent this, the module does not export the constructor for it---rather, the module exports a function `mkEvenInt' that creates an EvenInt if the given value is acceptable or raises an error otherwise. What's the right way to do this? Thanks! Brad Larsen

Show replies by date

gwern0＠gmail.com

19 Dec 19 Dec

2:20 a.m.

On 2007.12.18 21:07:25 -0500, Brad Larsen scribbled 0.6K characters:

...

Hi there list,

How would one go about creating a new type for a subset of the integers, for (contrived) example just the even integers? I was thinking of making a new type

newtype EvenInt = EvenInt Integer

but the problem with this is that it accepts any integer, even odd ones. So to prevent this, the module does not export the constructor for it---rather, the module exports a function `mkEvenInt' that creates an EvenInt if the given value is acceptable or raises an error otherwise.

What's the right way to do this? Thanks!

Brad Larsen

Well, I've had cause to do this in the past. Before I paste the following code, I'd like to emphasize that I wrote it a while when I was even more new to Haskell; that it compiles but hasn't been tested very much; and that I'm sure there are better ways to do it. What I wanted to do was to define a type for a subset of 'reals' (floats) which are either 0, or positive. The code looks like this:

...

{- For many equations and results, it is nonsensical to have negative results, > but we don't want to use solely natural numbers because then we lose precision. So we define a PosReal type which tries to define the subset of real numbers which are 0 or positive; this way the type system checks for negative results instead of every other function having conditionals checking for negative input or output. -} newtype PosReal = MakePosReal Float deriving (Show, Eq, Ord)

-- Basic numerical operations on positive reals instance Num PosReal where fromInteger = toPosReal . fromInteger x + y = MakePosReal (fromPosReal x + fromPosReal y) x - y = toPosReal ((fromPosReal x) - (fromPosReal y)) x * y = MakePosReal (fromPosReal x * fromPosReal y) abs x | x >= 0 = x | otherwise = x * (-1) signum x | x >= 0 = 1 | otherwise = (-1)

-- Define division on PosReals instance Fractional PosReal where x / y = toPosReal ((fromPosReal x) / (fromPosReal y)) fromRational x = MakePosReal (fromRational x)

-- Positive reals are truncated at 0 toPosReal :: Float -> PosReal toPosReal x | x < 0 = MakePosReal 0 | otherwise = MakePosReal x fromPosReal :: PosReal -> Float fromPosReal (MakePosReal i) = i

-- Define an instance to allow QuickCheck operations instance Arbitrary PosReal where arbitrary = liftM3 fraction arbitrary arbitrary arbitrary where fraction :: Integer -> Integer -> Integer -> PosReal fraction a b c = fromInteger a + (fromInteger b / (abs (fromInteger c) + 1))

-- gwern RFI el Audiotel muezzin E911 B61-11 Revolution 5.0i N5P6 espionage

Jules Bean

7 a.m.

Brad Larsen wrote:

...

Hi there list,

How would one go about creating a new type for a subset of the integers, for (contrived) example just the even integers? I was thinking of making a new type

newtype EvenInt = EvenInt Integer

but the problem with this is that it accepts any integer, even odd ones. So to prevent this, the module does not export the constructor for it---rather, the module exports a function `mkEvenInt' that creates an EvenInt if the given value is acceptable or raises an error otherwise.

What's the right way to do this? Thanks!

There are two ways: (1) Have a representation which admits invalid values, and provide combinators which only perfect validity, and prove that consumers using your combinators can't produce invalid values. (2) Have a cleverly designed representation such that every representation is valid. An example here, for (2) would be to store n/2; there is a bijection between 'Integer' and 'EvenInt' given by n/2. In real, more complex problems, (2) often isn't possible and we resort to (1). E.g. the representation of balanced trees (AVL? RedBlack?) admits invalid values (both unbalanced trees and out-of-order trees) and we rely on the reduced set of combinators never to generate one. Jules

Don Stewart

7:04 a.m.

jules:

...

Brad Larsen wrote:

...
Hi there list,

How would one go about creating a new type for a subset of the integers, for (contrived) example just the even integers? I was thinking of making a new type

newtype EvenInt = EvenInt Integer

but the problem with this is that it accepts any integer, even odd ones. So to prevent this, the module does not export the constructor for it---rather, the module exports a function `mkEvenInt' that creates an EvenInt if the given value is acceptable or raises an error otherwise.

What's the right way to do this? Thanks!

There are two ways:

(1) Have a representation which admits invalid values, and provide combinators which only perfect validity, and prove that consumers using your combinators can't produce invalid values.

(2) Have a cleverly designed representation such that every representation is valid.

An example here, for (2) would be to store n/2; there is a bijection between 'Integer' and 'EvenInt' given by n/2.

In real, more complex problems, (2) often isn't possible and we resort to (1). E.g. the representation of balanced trees (AVL? RedBlack?) admits invalid values (both unbalanced trees and out-of-order trees) and we rely on the reduced set of combinators never to generate one.

1) is always a challenge to particular types (heh) of people to do 2) We've a page on the wiki about this idiom, http://www.haskell.org/haskellwiki/Smart_constructors including links to type level enforcement. Last time I tried type level decimals they were still a little bit hairy. This might be easier now with type families though. -- Don

Derek Elkins

5:40 p.m.

On Tue, 2007-12-18 at 23:04 -0800, Don Stewart wrote:

...

jules:

...
Brad Larsen wrote:

...
Hi there list,

How would one go about creating a new type for a subset of the integers, for (contrived) example just the even integers? I was thinking of making a new type

newtype EvenInt = EvenInt Integer

but the problem with this is that it accepts any integer, even odd ones. So to prevent this, the module does not export the constructor for it---rather, the module exports a function `mkEvenInt' that creates an EvenInt if the given value is acceptable or raises an error otherwise.

What's the right way to do this? Thanks!

There are two ways:

(1) Have a representation which admits invalid values, and provide combinators which only perfect validity, and prove that consumers using your combinators can't produce invalid values.

(2) Have a cleverly designed representation such that every representation is valid.

An example here, for (2) would be to store n/2; there is a bijection between 'Integer' and 'EvenInt' given by n/2.

In real, more complex problems, (2) often isn't possible and we resort to (1). E.g. the representation of balanced trees (AVL? RedBlack?) admits invalid values (both unbalanced trees and out-of-order trees) and we rely on the reduced set of combinators never to generate one.

1) is always a challenge to particular types (heh) of people to do 2)

And indeed there are two distinct ways of enforcing balance in AVL trees using the type system. And of course, it would be "trivial" to do with dependent types. Usually the problem isn't so much that it is not possible, but that it is cumbersome and/or inefficient. http://www.haskell.org/pipermail/haskell/2003-April/011621.html http://www.haskell.org/pipermail/haskell/2003-April/011693.html (random) Also that month, lambdabot 1.0! http://www.haskell.org/pipermail/haskell/2003-April/011582.html

Brad Larsen

20 Dec 20 Dec

3:55 p.m.

On Wed, 19 Dec 2007 02:00:53 -0500, Jules Bean wrote:

...

Brad Larsen wrote:

...
Hi there list, How would one go about creating a new type for a subset of the integers, for (contrived) example just the even integers? I was thinking of making a new type newtype EvenInt = EvenInt Integer but the problem with this is that it accepts any integer, even odd ones. So to prevent this, the module does not export the constructor for it---rather, the module exports a function `mkEvenInt' that creates an EvenInt if the given value is acceptable or raises an error otherwise. What's the right way to do this? Thanks!

There are two ways:

(1) Have a representation which admits invalid values, and provide combinators which only perfect validity, and prove that consumers using your combinators can't produce invalid values.

(2) Have a cleverly designed representation such that every representation is valid.

An example here, for (2) would be to store n/2; there is a bijection between 'Integer' and 'EvenInt' given by n/2.

To make sure I understand, an example of (1) would be to export only a ``smart constructor'' that somehow converts invalid values to valid ones (say, add 1 to arguments that are odd)? In your example of 2, how would you go about storing n/2? Store just n as in (newtype EvenInt = EvenInt Integer) and then write all functions that deal with EvenInts so that they account for the division by two?

...

In real, more complex problems, (2) often isn't possible and we resort to (1). E.g. the representation of balanced trees (AVL? RedBlack?) admits invalid values (both unbalanced trees and out-of-order trees) and we rely on the reduced set of combinators never to generate one.

Jules

In my particular case, or what I actually want to do, is define a finite segment of the integers (0-42, say) as a new type and have that checked at compile time. Any way of doing this w/o defining Peano numbers or a whole bunch of nullary constructors (i.e. I'm hoping to be able to define a type whose constructor will accept only Integer arguments between 0 and 42)? Thanks! Brad

Jules Bean

4:05 p.m.

Brad Larsen wrote:

...

On Wed, 19 Dec 2007 02:00:53 -0500, Jules Bean wrote:

...
Brad Larsen wrote:

...
Hi there list, How would one go about creating a new type for a subset of the integers, for (contrived) example just the even integers? I was thinking of making a new type newtype EvenInt = EvenInt Integer but the problem with this is that it accepts any integer, even odd ones. So to prevent this, the module does not export the constructor for it---rather, the module exports a function `mkEvenInt' that creates an EvenInt if the given value is acceptable or raises an error otherwise. What's the right way to do this? Thanks!

There are two ways:

(1) Have a representation which admits invalid values, and provide combinators which only perfect validity, and prove that consumers using your combinators can't produce invalid values.

(2) Have a cleverly designed representation such that every representation is valid.

An example here, for (2) would be to store n/2; there is a bijection between 'Integer' and 'EvenInt' given by n/2.

To make sure I understand, an example of (1) would be to export only a ``smart constructor'' that somehow converts invalid values to valid ones (say, add 1 to arguments that are odd)?

I just meant one that throws a runtime error if they are not.

...

In your example of 2, how would you go about storing n/2? Store just n as in (newtype EvenInt = EvenInt Integer) and then write all functions that deal with EvenInts so that they account for the division by two?

You would store n/2. So "8" would be represented as EvenInt 4, "14" as EvenInt 7. Then you write the num instance to account for the division. Check out the num instance in Data.Fixed for an example.

...

...
In real, more complex problems, (2) often isn't possible and we resort to (1). E.g. the representation of balanced trees (AVL? RedBlack?) admits invalid values (both unbalanced trees and out-of-order trees) and we rely on the reduced set of combinators never to generate one.

Jules

In my particular case, or what I actually want to do, is define a finite segment of the integers (0-42, say) as a new type and have that checked at compile time. Any way of doing this w/o defining Peano numbers or a whole bunch of nullary constructors (i.e. I'm hoping to be able to define a type whose constructor will accept only Integer arguments between 0 and 42)?

Not at compile-time, no. The best you can do is runtime error. There is no compile-time facility to check that an Int lies in a particular range. Consider, for example, that the int might not be known at compiletime: do id <- myThreadID return (MkSmallInt id) ^^ how can the compiler know? In general, of course, the question of calculating if an int is under 42 at compile time is the question of partial evaluation. Partial evaluation at compile time is flat-out impossible for IO actions, and although it's possible for pure functions, GHC doesn't do it to any significant extent. (It would make the compiler potentially non-terminating, of course!) Jules

6404

Age (days ago)

6405

Last active (days ago)

List overview

Download

6 comments

5 participants

participants (5)

Brad Larsen
Derek Elkins
Don Stewart
gwern0＠gmail.com
Jules Bean