Send Beginners mailing list submissions to
[email protected]
To subscribe or unsubscribe via the World Wide Web, visit
http://www.haskell.org/mailman/listinfo/beginners
or, via email, send a message with subject or body 'help' to
[email protected]
You can reach the person managing the list at
[email protected]
When replying, please edit your Subject line so it is more specific
than "Re: Contents of Beginners digest..."
Today's Topics:
1. Re: Further constraining types (Daniel Fischer)
2. Re: Looking for alternative practices suggestions (Brent Yorgey)
3. Re: Further constraining types (Brent Yorgey)
4. Re: Further constraining types (Christopher Howard)
5. Re: Further constraining types (Christopher Howard)
6. Re: Further constraining types (David Virebayre)
7. Re: Looking for alternative practices suggestions
(Michael Litchard)
8. Re: Further constraining types (Brent Yorgey)
9. Re: Looking for alternative practices suggestions
(Heinrich Apfelmus)
----------------------------------------------------------------------
Message: 1
Date: Fri, 5 Aug 2011 12:50:10 +0200
From: Daniel Fischer <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: [email protected]
Message-ID: <[email protected]>
Content-Type: Text/Plain; charset="iso-8859-1"
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.)
------------------------------
Message: 2
Date: Fri, 5 Aug 2011 09:51:28 -0400
From: Brent Yorgey <[email protected]>
Subject: Re: [Haskell-beginners] Looking for alternative practices
suggestions
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
On Thu, Aug 04, 2011 at 02:53:34PM -0700, Michael Litchard wrote:
> I'm finding that in more than one instance I pass a data structure to
> a function, simply so that I can pass it to it's helper function. It
> bugs me that I'm passing a value that isn't being used directly. This
> seems wrong. Example: I have a "data URLSequence" that contains a way
> to calculate the ip address of a URL. This gets passed to a helper
> function that generates a particular URL, which then populates the
> URLSequence. Is there a standard practice to avoid what I am talking
> about? Or is this normal and I should accept it?
Others have answered the question in a way that seems to address your
situation well. However, I thought I would also mention that in the
case where there is a single piece of read-only data that needs to be
annoyingly threaded through large parts of your code, you can use the
Reader monad to make the threading implicit. But this solution is too
heavyweight for some situations since it does require changing the
code to use a monadic style.
-Brent
------------------------------
Message: 3
Date: Fri, 5 Aug 2011 10:00:16 -0400
From: Brent Yorgey <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: Christopher Howard <[email protected]>
Cc: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
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
------------------------------
Message: 4
Date: Fri, 05 Aug 2011 06:55:19 -0800
From: Christopher Howard <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: Haskell Beginners <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
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
------------------------------
Message: 5
Date: Fri, 05 Aug 2011 06:56:38 -0800
From: Christopher Howard <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: Haskell Beginners <[email protected]>
Message-ID: <[email protected]>
Content-Type: text/plain; charset=ISO-8859-1; format=flowed
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
------------------------------
Message: 6
Date: Fri, 5 Aug 2011 17:57:24 +0200
From: David Virebayre <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: Brent Yorgey <[email protected]>
Cc: [email protected]
Message-ID:
<CAM_wFVsKd4Kxiaj8QQf=fwvx+obynvcufsk0oppx-kt9swa...@mail.gmail.com>
Content-Type: text/plain; charset=UTF-8
2011/8/5 Brent Yorgey <[email protected]>:
> 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
------------------------------
Message: 7
Date: Fri, 5 Aug 2011 13:04:54 -0700
From: Michael Litchard <[email protected]>
Subject: Re: [Haskell-beginners] Looking for alternative practices
suggestions
To: Brent Yorgey <[email protected]>
Cc: [email protected]
Message-ID:
<caezekyqesyohqjy12rdujosydq7p9ynjsxtchs0b8jqo5qq...@mail.gmail.com>
Content-Type: text/plain; charset=ISO-8859-1
Thanks Brent. I just may use a Reader monad in version 2 for the sake
of learning how to do it.
On Fri, Aug 5, 2011 at 6:51 AM, Brent Yorgey <[email protected]> wrote:
> On Thu, Aug 04, 2011 at 02:53:34PM -0700, Michael Litchard wrote:
>> I'm finding that in more than one instance I pass a data structure to
>> a function, simply so that I can pass it to it's helper function. It
>> bugs me that I'm passing a value that isn't being used directly. This
>> seems wrong. Example: I have a "data URLSequence" that contains a way
>> to calculate the ip address of a URL. This gets passed to a helper
>> function that generates a particular URL, which then populates the
>> URLSequence. Is there a standard practice to avoid what I am talking
>> about? Or is this normal and I should accept it?
>
> Others have answered the question in a way that seems to address your
> situation well. ?However, I thought I would also mention that in the
> case where there is a single piece of read-only data that needs to be
> annoyingly threaded through large parts of your code, you can use the
> Reader monad to make the threading implicit. ?But this solution is too
> heavyweight for some situations since it does require changing the
> code to use a monadic style.
>
> -Brent
>
> _______________________________________________
> Beginners mailing list
> [email protected]
> http://www.haskell.org/mailman/listinfo/beginners
>
------------------------------
Message: 8
Date: Fri, 5 Aug 2011 17:10:56 -0400
From: Brent Yorgey <[email protected]>
Subject: Re: [Haskell-beginners] Further constraining types
To: Christopher Howard <[email protected]>
Cc: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=us-ascii
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
------------------------------
Message: 9
Date: Sat, 06 Aug 2011 08:57:19 +0200
From: Heinrich Apfelmus <[email protected]>
Subject: Re: [Haskell-beginners] Looking for alternative practices
suggestions
To: [email protected]
Message-ID: <[email protected]>
Content-Type: text/plain; charset=UTF-8; format=flowed
Michael Litchard wrote:
> I'm finding that in more than one instance I pass a data structure to
> a function, simply so that I can pass it to it's helper function. It
> bugs me that I'm passing a value that isn't being used directly. This
> seems wrong. Example: I have a "data URLSequence" that contains a way
> to calculate the ip address of a URL. This gets passed to a helper
> function that generates a particular URL, which then populates the
> URLSequence. Is there a standard practice to avoid what I am talking
> about? Or is this normal and I should accept it?
An old blog post by Duncan Coutts describes how to eliminate some
parameter passing with higher-order functions (essentially continuations):
http://www.well-typed.com/blog/10
Best regards,
Heinrich Apfelmus
--
http://apfelmus.nfshost.com
------------------------------
_______________________________________________
Beginners mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/beginners
End of Beginners Digest, Vol 38, Issue 10
*****************************************
