Further constraining types

Christopher Howard

4 Aug 2011 4 Aug '11

5:03 a.m.

Let's say I have "f", which is a function of the following type: f :: Int -> Int However, let's say f is only capable of handling positive integers. Let's say that I'm committed to making f a complete function in the sense that (1) the pattern matching of the function is always complete and (2) there are no internal aborts, like an "error" call or an "undefined" expression. Obviously I could change the type to f :: Int -> Maybe Int ...to deal with the case where a negative parameter is passed in. But it seems like what I really want is something like this: f :: Positive Int -> Int I.e., the "positiveness" is hard-coded into the parameter type. But how do I do this? I was thinking it would involve some kind of "Positive Int" type, and some kind of "constructor" function like so: positiveNum :: Int -> Positive Int However, then this constructor function must deal with the problem of receiving a negative integer, and thus I have only shifted the problem. It is still an improvement, but yet it seems like I am missing some important concept here... -- frigidcode.com theologia.indicium.us

Show replies by date

Brandon Allbery

4 Aug 4 Aug

5:23 a.m.

On Thu, Aug 4, 2011 at 01:03, Christopher Howard < christopher.howard@frigidcode.com> wrote:

...

...to deal with the case where a negative parameter is passed in. But it seems like what I really want is something like this:

f :: Positive Int -> Int

I.e., the "positiveness" is hard-coded into the parameter type. But how do I do this? I was thinking it would involve some kind of "Positive Int" type, and some kind of "constructor" function like so:

positiveNum :: Int -> Positive Int

However, then this constructor function must deal with the problem of receiving a negative integer, and thus I have only shifted the problem. It is still an improvement, but yet it seems like I am missing some important concept here...

The concept is called "dependent types", where a type can depend on a value. Haskell doesn't support them natively, although there are some hacks for limited cases. -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Christopher Howard

6:51 a.m.

On 08/03/2011 09:23 PM, Brandon Allbery wrote:

...

On Thu, Aug 4, 2011 at 01:03, Christopher Howard mailto:christopher.howard@frigidcode.com> wrote:

...to deal with the case where a negative parameter is passed in. But it seems like what I really want is something like this:

f :: Positive Int -> Int

I.e., the "positiveness" is hard-coded into the parameter type. But how do I do this? I was thinking it would involve some kind of "Positive Int" type, and some kind of "constructor" function like so:

positiveNum :: Int -> Positive Int

However, then this constructor function must deal with the problem of receiving a negative integer, and thus I have only shifted the problem. It is still an improvement, but yet it seems like I am missing some important concept here...

The concept is called "dependent types", where a type can depend on a value. Haskell doesn't support them natively, although there are some hacks for limited cases.

-- brandon s allbery allbery.b@gmail.com mailto:allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

This seems like a really significant issue for a functional programming language. Am I eventually going to have to switch to Agda? My friends are trying to convert me... -- frigidcode.com theologia.indicium.us

David Virebayre

8:03 a.m.

2011/8/4 Christopher Howard :

...

On 08/03/2011 09:23 PM, Brandon Allbery wrote:

...

This seems like a really significant issue for a functional programming language. Am I eventually going to have to switch to Agda? My friends are trying to convert me...

I don't know Agda and what dependent type guarantee, but I don't see how they would prevent a user typing '-123' where you expect a positive number, so one way or another you will have to deal with input at runtime. Once you've validated your user input though, nothing prevents you to have it return a Positive Int that you will guarantee can hold only positive integers, for example by using a smart constructor, and hiding the contructor in a separate module. You don't need dependant types for this. David.

Thomas

10:49 a.m.

...

Once you've validated your user input though, nothing prevents you to have it return a Positive Int that you will guarantee can hold only positive integers, for example by using a smart constructor, and hiding the contructor in a separate module. You don't need dependant types for this.

Yes, but once you want to operate on that data you'll note the difference: subtract :: Positive Int -> Positive Int -> ??? IIUC with dependent types you'll have a compile time guarantee, without you'll have to test for errors at runtime. Regards, Thomas

Christopher Howard

5 Aug 5 Aug

2:52 a.m.

On 08/04/2011 12:03 AM, David Virebayre wrote:

...

2011/8/4 Christopher Howard:

...
On 08/03/2011 09:23 PM, Brandon Allbery wrote:

...
This seems like a really significant issue for a functional programming language. Am I eventually going to have to switch to Agda? My friends are trying to convert me...

I don't know Agda and what dependent type guarantee, but I don't see how they would prevent a user typing '-123' where you expect a positive number, so one way or another you will have to deal with input at runtime.

Once you've validated your user input though, nothing prevents you to have it return a Positive Int that you will guarantee can hold only positive integers, for example by using a smart constructor, and hiding the contructor in a separate module. You don't need dependant types for this.

David.

But users are not the only source of ints. For example, let's say I wanted to do my own square function, with a type like so: square :: Int -> Positive Int So, I use the special constructor function in the implementation: square x = validatePositive $ x * x Great! now I have a function that returns Positive Ints, which can be fed into any function that takes a Positive Int as its parameter. Problem, though... how do I implement this special constructor in a way that meets the criteria for completeness that I outlined earlier? A validation function, by definition, allows for the possibility of invalidation. So the type would have to be: validatePositive :: Int -> Maybe (Positive Int) But this means the type of square would have to be changed to square :: Int -> Maybe (Positive Int) ...which is unacceptable. (I /know/ square /will/ always return an positive integer, not that it /might/ do so!) I could of course throw a "maybe"-style forced cast into the square function, but that would defeat one of the fundamental principles of what I'm trying to accomplish here. Anyway, I think Brandon is right and the answer is in dependent types, though to be honest I'm having real trouble decoding any of the literature I've found so far. -- frigidcode.com theologia.indicium.us

David Virebayre

7:17 a.m.

2011/8/5 Christopher Howard :

...

But users are not the only source of ints. For example, let's say I wanted to do my own square function, with a type like so:

...

square :: Int -> Positive Int validatePositive :: Int -> Maybe (Positive Int)

...

But this means the type of square would have to be changed to square :: Int -> Maybe (Positive Int)

I would go with : validatePositive :: Int -> Maybe (Positive Int) square :: Positive Int -> Positive Int For the subtraction problem as shown by Thomas, you can subtract :: Positive Int -> Positive Int -> Maybe (Positive Int) subtract (Positive a) (Positive b) | a >= b = Just $ Positive (a-b) | otherwise = Nothing But that's what you want to avoid, so maybe it's acceptable, depending on your problem, to do: subtract :: Positive Int -> Positive Int -> Positive Int subtract (Positive a) (Positive b) | a >= b = Positive (a-b) | otherwise = Positive 0 The only other solution would be to statically guarantee that a>b, with dependent types you could probably; but since I know next to nothing about that, I have trouble seeing how could work with a simple example like that: (and I would love to learn !) 1 - read two lines from stdin 2 - convert each lines to natural numbers a and b 3 - subtract b from a , a>b should be statically guaranteed 4 - print the result David.

Arlen Cuss

7:22 a.m.

...

I would go with : validatePositive :: Int -> Maybe (Positive Int) square :: Positive Int -> Positive Int

But squaring a negative Int is still guaranteed to be positive!

David Virebayre

7:44 a.m.

2011/8/5 Arlen Cuss :

...

...
I would go with : validatePositive :: Int -> Maybe (Positive Int) square :: Positive Int -> Positive Int

But squaring a negative Int is still guaranteed to be positive!

I thought he said he wanted to work with natural numbers. David.

Daniel Fischer

10:50 a.m.

On Friday 05 August 2011, 04:52:03, Christopher Howard wrote:

...

But this means the type of square would have to be changed to

square :: Int -> Maybe (Positive Int)

...which is unacceptable. (I know square will always return an positive integer, not that it might do so!)

As for Int, that's not true: Prelude> 4000000000^2 :: Int -2446744073709551616 The square of an Integer will be nonnegative (or kill your process by OOM), but to decide whether something could return a (Positive Foo) instead of a (Maybe (Positive Foo)), you have to take Foo's semantics into account in addition to the abstract mathematical properties of the algorithm. (Tangential to your point, but nevertheless.)

Christopher Howard

2:56 p.m.

On 08/05/2011 02:50 AM, Daniel Fischer wrote:

...

On Friday 05 August 2011, 04:52:03, Christopher Howard wrote:

...
But this means the type of square would have to be changed to

square :: Int -> Maybe (Positive Int)

...which is unacceptable. (I know square will always return an positive integer, not that it might do so!)

As for Int, that's not true:

Prelude> 4000000000^2 :: Int -2446744073709551616

The square of an Integer will be nonnegative (or kill your process by OOM), but to decide whether something could return a (Positive Foo) instead of a (Maybe (Positive Foo)), you have to take Foo's semantics into account in addition to the abstract mathematical properties of the algorithm.

(Tangential to your point, but nevertheless.)

*my head explodes* Guess I'll have to use Integers from now on. -- frigidcode.com theologia.indicium.us

Brent Yorgey

2 p.m.

On Thu, Aug 04, 2011 at 06:52:03PM -0800, Christopher Howard wrote:

...

Anyway, I think Brandon is right and the answer is in dependent types, though to be honest I'm having real trouble decoding any of the literature I've found so far.

I recommend reading "The Power of Pi" by Oury and Swierstra (http://www.cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf). It's a very readable introduction to dependently-typed programming with several great examples. Your particular problem could be solved by creating a type Positive which consists of an Integer value paired with a *proof* that it is positive. Then the squaring function (for example) could exploit the properties of multiplication to return the result along with a proof I realize that's a bit vague; I could explain how this would work in more detail if you like. -Brent

Christopher Howard

2:55 p.m.

On 08/05/2011 06:00 AM, Brent Yorgey wrote:

...

On Thu, Aug 04, 2011 at 06:52:03PM -0800, Christopher Howard wrote:

...
Anyway, I think Brandon is right and the answer is in dependent types, though to be honest I'm having real trouble decoding any of the literature I've found so far.

I recommend reading "The Power of Pi" by Oury and Swierstra (http://www.cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf). It's a very readable introduction to dependently-typed programming with several great examples.

I'll read through the link this weekend.

...

Your particular problem could be solved by creating a type Positive which consists of an Integer value paired with a *proof* that it is positive. Then the squaring function (for example) could exploit the properties of multiplication to return the result along with a proof I realize that's a bit vague; I could explain how this would work in more detail if you like.

-Brent

Are you saying that is how I would do it Agda, or is there a way to do that in Haskell? More detail would be great. -- frigidcode.com theologia.indicium.us

Brent Yorgey

9:10 p.m.

On Fri, Aug 05, 2011 at 06:55:19AM -0800, Christopher Howard wrote:

...

On 08/05/2011 06:00 AM, Brent Yorgey wrote:

...
On Thu, Aug 04, 2011 at 06:52:03PM -0800, Christopher Howard wrote:

...
Anyway, I think Brandon is right and the answer is in dependent types, though to be honest I'm having real trouble decoding any of the literature I've found so far.

I recommend reading "The Power of Pi" by Oury and Swierstra (http://www.cs.ru.nl/~wouters/Publications/ThePowerOfPi.pdf). It's a very readable introduction to dependently-typed programming with several great examples.

I'll read through the link this weekend.

...
Your particular problem could be solved by creating a type Positive which consists of an Integer value paired with a *proof* that it is positive. Then the squaring function (for example) could exploit the properties of multiplication to return the result along with a proof I realize that's a bit vague; I could explain how this would work in more detail if you like.

-Brent

Are you saying that is how I would do it Agda, or is there a way to do that in Haskell? More detail would be great.

Sorry, I meant this is how you would do it in Agda. It is not possible to do this directly in Haskell (because Haskell does not have dependent types). (There are ways of "faking" some dependent types in Haskell with type-level-programming techniques... but they can be quite convoluted and would definitely be taking this email too far afield.) Why are dependent types required? To see that, a bit of background first. A *proof* is a term, whose *type* describes the proposition of which it is a proof. For example, the proposition (P -> Q) read "P implies Q", has as its proofs functions which take a proof of P (that is, a value of type P) and produce a proof of Q. This correspondence between (terms, types) and (proofs, propositions) is known as the Curry-Howard Isomorphism. However, I said we wanted to pair a number n with a proof that (n > 0) -- so the *proposition/type* (n > 0) needs to mention the *term-level variable* n, so in order to state this we would have to have types which can depend on terms. Agda can do this; Haskell cannot. My Agda is too rusty at the moment to actually show you some code that would accomplish this. But the basic idea would be essentially what I already said above: we could define the type Positive as a pair of an integer together with a proof that it is greater than zero; then if we wanted to write a function square :: Integer -> Positive we would be required to give not only the result of squaring the input number, but also a *proof* that this result is always greater than zero. ...but actually, this is false! What if the input is zero? Of course, this is part of the value of having your proofs checked by a machine. =) If we change Positive to NonNegative and require a proof just that the number is greater than or equal to zero, we could then generate the proof for square without too much trouble given the definitions of multiplication and greater-than. If you want to learn more about the Curry-Howard Isomorphism and computer-assisted proofs in general, I recommend reading (the first few chapters of) Software Foundations: http://www.cis.upenn.edu/~bcpierce/sf/ -Brent

Christopher Howard

6 Aug 6 Aug

7:39 p.m.

On 08/05/2011 01:10 PM, Brent Yorgey wrote:

...

Sorry, I meant this is how you would do it in Agda. It is not possible to do this directly in Haskell (because Haskell does not have dependent types). (There are ways of "faking" some dependent types in Haskell with type-level-programming techniques... but they can be quite convoluted and would definitely be taking this email too far afield.)

{- Supposing for now we set aside dependent types, I'm thinking that the closest I get to my ideal is a combination of safe constructors and law-style rewriting. I'm thinking this could be workable: -} module Natural ( Natural(), natural, (==), (+), (-), (*), abs, signum, fromInteger ) where data Natural = Natural Integer | Indeterminate deriving (Show) -- fundamental constructor natural :: Integer -> Natural natural n | n < 0 = Indeterminate natural n = Natural n -- trying to fit it into the Num class instance Eq Natural where -- very controversial, but necessary to satisfy signum law (==) Indeterminate Indeterminate = True (==) Indeterminate _ = False (==) _ Indeterminate = False (==) (Natural a) (Natural b) | a == b = True | otherwise = False instance Num Natural where Indeterminate + _ = Indeterminate _ + Indeterminate = Indeterminate (Natural a) + (Natural b) = Natural ((Prelude.+) a b) Indeterminate - _ = Indeterminate _ - Indeterminate = Indeterminate (Natural a) - (Natural b) | a < b = Indeterminate | otherwise = Natural ((Prelude.-) a b) Indeterminate * _ = Indeterminate _ * Indeterminate = Indeterminate (Natural a) * (Natural b) | a < 0 || b < 0 = Indeterminate | otherwise = Natural ((Prelude.*) a b) abs Indeterminate = Indeterminate abs (Natural a) = (Natural a) signum Indeterminate = Indeterminate signum (Natural 0) = (Natural 0) signum (Natural a) = (Natural 1) fromInteger n = natural n {- Fundamentally, this is not really much different than using a constructor that returns a Maybe value. But it does gives me a much more "natural" type syntax, while still allowing my calculations to error-out without bottoms or crashes. Thoughts? -} -- frigidcode.com theologia.indicium.us

Thomas

8:54 p.m.

...

(==) (Natural a) (Natural b) | a == b = True | otherwise = False

Essentially the same, but I usually write this a little shorter as (==) (Natural a) (Natural b) = a == b

...

(Natural a) * (Natural b) | a < 0 || b < 0 = Indeterminate | otherwise = Natural ((Prelude.*) a b)

Why this? A 'Natural x' should already guarantee that 'x' is not negative (otherwise it would be 'Indeterminate').

...

Thoughts?

It seems very reasonable to me. Regards, Thomas

Christopher Howard

7 Aug 7 Aug

5:54 a.m.

On 08/06/2011 12:54 PM, Thomas wrote:

...

...
(==) (Natural a) (Natural b) | a == b = True | otherwise = False

Essentially the same, but I usually write this a little shorter as (==) (Natural a) (Natural b) = a == b

...
(Natural a) * (Natural b) | a < 0 || b < 0 = Indeterminate | otherwise = Natural ((Prelude.*) a b)

Why this? A 'Natural x' should already guarantee that 'x' is not negative (otherwise it would be 'Indeterminate').

...
Thoughts?

It seems very reasonable to me.

Regards, Thomas

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

One more quick question: If I hide my actual constructors in favor of a smart constructor, is it no longer possible for me to do direct pattern matching on the values? E.g., the compiler does not allow this: analyze (Natural 5) = "It's a five!!!" ...so I have to do this: analyze a | natural 5 = "It's a five!!!" -- frigidcode.com theologia.indicium.us

Antoine Latter

6:08 a.m.

On Sun, Aug 7, 2011 at 12:54 AM, Christopher Howard

...

One more quick question: If I hide my actual constructors in favor of a smart constructor, is it no longer possible for me to do direct pattern matching on the values? E.g., the compiler does not allow this:

analyze (Natural 5) = "It's a five!!!"

...so I have to do this:

analyze a | natural 5 = "It's a five!!!"

You can use non-standard GHC extensions: Given a function: someView :: Natural a -> a you can pattern match like so: case myNat of (someView -> 5) -> "It's a five!!!" This requires {-# LANGUAGE ViewPatterns #-} at the top of your source file to enable. Antoine

...

-- frigidcode.com theologia.indicium.us

_______________________________________________ Beginners mailing list Beginners@haskell.org http://www.haskell.org/mailman/listinfo/beginners

Henk-Jan van Tuyl

9:36 a.m.

On Sun, 07 Aug 2011 08:08:31 +0200, Antoine Latter wrote:

...

You can use non-standard GHC extensions:

Given a function:

someView :: Natural a -> a

you can pattern match like so:

case myNat of (someView -> 5) -> "It's a five!!!"

This requires {-# LANGUAGE ViewPatterns #-} at the top of your source file to enable.

Not using any extension: case fromNatural myNat of 5 -> "It's a five!!!" The function fromNatural is, of course, imported from the module defining Natural. Regards, Henk-Jan van Tuyl -- http://Van.Tuyl.eu/ http://members.chello.nl/hjgtuyl/tourdemonad.html --

David Virebayre

5 Aug 5 Aug

3:57 p.m.

2011/8/5 Brent Yorgey :

...

Your particular problem could be solved by creating a type Positive which consists of an Integer value paired with a *proof* that it is positive. Then the squaring function (for example) could exploit the properties of multiplication to return the result along with a proof I realize that's a bit vague; I could explain how this would work in more detail if you like.

I realiser the offer wasn't for me but yes, please, I'd like to know how you could do that, also with a subtract function example, and with a user input example. Pretty please ? David

Brandon Allbery

4:29 a.m.

On Thu, Aug 4, 2011 at 02:51, Christopher Howard < christopher.howard@frigidcode.com> wrote:

...

On 08/03/2011 09:23 PM, Brandon Allbery wrote:

...
The concept is called "dependent types", where a type can depend on a value. Haskell doesn't support them natively, although there are some hacks for limited cases.

This seems like a really significant issue for a functional programming language. Am I eventually going to have to switch to Agda? My friends are trying to convert me...

Agda is a wonderful FP platform, but I'm not convinced Agda is at all ready to be an *applications* platform. So if theory is your thing, go straight to Agda; if you want to use FP for real world problems, Haskell is (at least for now) a better choice. (Or OCaml, but you then lose the advantages of purity on top of not having dependent types.) -- brandon s allbery allbery.b@gmail.com wandering unix systems administrator (available) (412) 475-9364 vm/sms

Arlen Cuss

4 Aug 4 Aug

7:36 a.m.

04.08.2011 15:03, Christopher Howard kirjutas:

...

Let's say I have "f", which is a function of the following type:

f :: Int -> Int

However, let's say f is only capable of handling positive integers. Let's say that I'm committed to making f a complete function in the sense that (1) the pattern matching of the function is always complete and (2) there are no internal aborts, like an "error" call or an "undefined" expression. Obviously I could change the type to

f :: Int -> Maybe Int

...to deal with the case where a negative parameter is passed in. But it seems like what I really want is something like this:

f :: Positive Int -> Int

I.e., the "positiveness" is hard-coded into the parameter type. But how do I do this? I was thinking it would involve some kind of "Positive Int" type, and some kind of "constructor" function like so:

positiveNum :: Int -> Positive Int

However, then this constructor function must deal with the problem of receiving a negative integer, and thus I have only shifted the problem. It is still an improvement, but yet it seems like I am missing some important concept here...

What about positiveNum :: Int -> Maybe (Positive Int)? The reality is you need to provide a way to get some Int to Positive Int, and since Haskell doesn't have the notion of a positive-only Int built in, you need to be prepared that a non-positive Int might get through to your constructor at runtime. After that, you're set!

5080

Age (days ago)

5083

Last active (days ago)

List overview

Download

21 comments

9 participants

participants (9)

Antoine Latter
Arlen Cuss
Brandon Allbery
Brent Yorgey
Christopher Howard
Daniel Fischer
David Virebayre
Henk-Jan van Tuyl
Thomas