Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 11:21 AM, Conal Elliott wrote:

> 
> And I also raised a more fundamental question than whether this claim of 
> sameness is true, namely what is equality on IO? Without a precise & 
> consistent definition of equality, the claims like "f 42 == f (43 - 1)" are 
> even defined, let alone true. And since the conversation is about Haskell IO, 
> I'm looking for a definition that applies to all of IO, not just some 
> relatively well-behaved subset like putchar/getchar+IORefs+threads.

Well, you'll no doubt be glad to know I think I've said about all I need to say 
on this topic, but I'll add one more thing.  Threads like this I often find 
useful even when I disagree vehemently with various parties.  In this case an 
old idea I'd forgotten about was suddenly dislodged by the discussion.  A few 
years ago - the last time I got involved in a discussion on Haskell semantics - 
I spent some time sketching out ideas for using random variables to provide 
definitions (or at least notation) for stuff like IO.  I'm not sure I could 
even find the notes now, but my recollection is that it seemed like a promising 
approach.  One advantage is that this eliminates the kind of informal language 
(like "user input") that seems unavoidable in talking about IO.  Instead of 
defining e.g. readChar or the like as an "action" that does something and 
returns an char (or however standard Haskell idiom puts it), you can just say 
that readChar is a random char variable and be done with it.  The notion of 
"doing an action" goes away.  The side-effect of actually reading the input or 
the like can be defined generically by saying that evaluating a random variable 
always has some side-effect; what specifically the side effect is does not 
matter.  I mention this as a possible approach for anybody looking for a better 
way of accounting for IO in Haskell.

Cheers,

Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 11:43 AM, Conal Elliott wrote:
>> roof: f is a function, and it is taking the same argument each time. 
>> Therefore the result is the same each time.
> 
> That's called begging the question.  f is not a function, so I guess your 
> proof is flawed.
> 
> It seems pretty clear that we're working with different ideas of what 
> constitutes a function.  When I use the term, I intend what I take to be the 
> standard notion of a function in computation: not just a unique mapping from 
> one input to one output, but one where the output is computable from the 
> input.  Any "function" that depends on a non-computable component is by that 
> definition not a true function.  For clarity let's call such critters  
> quasi-functions, so we can retain the notion of application.  Equality cannot 
> be defined for quasi-functions, for obvious reasons.
> 
> f is a quasi-function because it depends on getAnIntFromUser, which is not 
> definable and is obviously not a function.  When applied to an argument like 
> 42, it yields another quasi-function, and therefore "f 42 = f 42" is false, 
> or at least unknown, and the same goes for f 42 != f 42 I suppose.  
> 
> -Gregg
> 
> Please don't redefine "function" to mean "computable function". Besides 
> distancing yourself from math, I don't think doing so really helps your case.

No redefinition involved, just a narrowing of scope.  I assume that, since we 
are talking about computation, it is reasonable to limit  the discussion to the 
class of computable functions - which, by the way, are about as deeply embedded 
in orthodox mathematics as you can get, by way of recursion theory.  What would 
be the point of talking about non-computable functions for the semantics of a 
programming language?

> And on what do you base your claim that getAnIntFromUser is not definable?

Sorry, not definable might a little strong.  "Not definable in the way we can 
define computable functions" work better?  In any case I think you probably see 
what I'm getting at.

> Or that applying it (what?) to 42 gives a quasi-function?

I can't think of a way to improve on what I've already written at the moment - 
it too would depend on IO - so if my meaning is not clear, so be it.

Wait, here's another way of looking at it.  Think of IO actions as random 
variables.  So instead of getAnIntFromUser, use X as an integer random variable 
yielding something like:

 f :: Int -> IO Int
 f x = X >>= \i -> return (i+x)

I would not call this f a function because I don't think it answers to the 
commonly accepted definition of a function.  Ditto for the result of applying 
it to 42.  Others obviously might consider it a function.  De gustibus non set 
disputandem.

-Gregg

-Gregg___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 11:19 AM, Heinrich Apfelmus wrote:

> Conal Elliott wrote:
>> Heinrich Apfelmus wrote:
>>> The function
>>> 
>>> f :: Int -> IO Int
>>> f x = getAnIntFromTheUser >>= \i -> return (i+x)
>>> 
>>> is pure according to the common definition of "pure" in the context of
>>> purely functional programming. That's because
>>> 
>>> f 42 = f (43-1) = etc.
>>> 
>>> Put differently, the function always returns the same IO action, i.e. the
>>> same value (of type  IO Int) when given the same parameter.
>>> 
>> Two questions trouble me:
>> How can we know whether this claim is true or not?
>> What does the claim even mean, i.e., what does "the same IO action" mean,
>> considering that we lack a denotational model of IO?
> 
> I think you can put at least these troubles to rest by noting that  f 42  and 
>  f (43-1)  are intentionally equal, even though you're not confident on their 
> extensional meaning.

(I think you meant "intensionally").  Ok, I think I can go with that, something 
like "f 42 means the sum of 42 and the user input".  And I suppose one could 
argue that the extension of f is well-defined as the set of integer pairs.  But 
that does not make f a (computable) function, because the mapping from domain 
to co-domain remains undefined, dependent as it is on IO.

-Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 11:11 AM, Chris Smith wrote:

> 
>> time t:  f 42   (computational process implementing func application
>> begins…)
>> t+1:= 1
>> t+2:  43   (… and ends)
>> 
>> 
>> time t+3:  f 42
>> t+4:   = 2
>> t+5:  44
>> 
>> 
>> Conclusion:  f 42 != f 42
> 
> That conclusion would only follow if the same IO action always produced
> the same result when performed twice in a row.  That's obviously untrue,
> so the conclusion doesn't follow.  What you've done is entirely
> consistent with the fact that f 42 = f 42... it just demonstrates that
> whatever f 42 is, it doesn't always produce the same result when you o
> it twice.
> 
> What Conal is getting at is that we don't have a formal model of what an
> IO action means.

Right, and my little counter-example is intended to support that.

>  Nevertheless, we know because f is a function

We do?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 11:20 AM, Colin Adams wrote:

> 
> On 30 December 2011 17:17, Gregg Reynolds  wrote:
> 
> On Dec 30, 2011, at 11:04 AM, Colin Adams wrote:
> 
>> 
>> 
>> On 30 December 2011 16:59, Gregg Reynolds  wrote:
>> 
>>> On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus 
>>>  wrote:
>>> 
>>> The function
>>> 
>>>  f :: Int -> IO Int
>>>  f x = getAnIntFromTheUser >>= \i -> return (i+x)
>>> 
>>> is pure according to the common definition of "pure" in the context of 
>>> purely functional programming. That's because
>>> 
>>>  f 42 = f (43-1) = etc.
>>> 
>> Conclusion:  f 42 != f 42
>> 
>> (This seems so extraordinarily obvious that maybe Heinrich has something 
>> else in mind.)
>> 
>> This seems such an obviously incorrect conclusion.
>> 
>> f42 is a funtion for returning a program for returning an int, not a 
>> function for returning an int.
> 
> 
> My conclusion holds:  f 42 != f 42.  Obviously, so I won't burden you with an 
> explanation. ;)
> 
> -Gregg
> Your conclusion is clearly erroneous.
> 
> proof: f is a function, and it is taking the same argument each time. 
> Therefore the result is the same each time.

That's called begging the question.  f is not a function, so I guess your proof 
is flawed.

It seems pretty clear that we're working with different ideas of what 
constitutes a function.  When I use the term, I intend what I take to be the 
standard notion of a function in computation: not just a unique mapping from 
one input to one output, but one where the output is computable from the input. 
 Any "function" that depends on a non-computable component is by that 
definition not a true function.  For clarity let's call such critters  
quasi-functions, so we can retain the notion of application.  Equality cannot 
be defined for quasi-functions, for obvious reasons.

f is a quasi-function because it depends on getAnIntFromUser, which is not 
definable and is obviously not a function.  When applied to an argument like 
42, it yields another quasi-function, and therefore "f 42 = f 42" is false, or 
at least unknown, and the same goes for f 42 != f 42 I suppose.  

-Gregg___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 11:04 AM, Colin Adams wrote:

> 
> 
> On 30 December 2011 16:59, Gregg Reynolds  wrote:
> 
>> On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus 
>>  wrote:
>> 
>> The function
>> 
>>  f :: Int -> IO Int
>>  f x = getAnIntFromTheUser >>= \i -> return (i+x)
>> 
>> is pure according to the common definition of "pure" in the context of 
>> purely functional programming. That's because
>> 
>>  f 42 = f (43-1) = etc.
>> 
>> Put differently, the function always returns the same IO action, i.e. the 
>> same value (of type  IO Int) when given the same parameter.
>> 
>> 
> 
> 
> time t:  f 42   (computational process implementing func application begins…)
> t+1:= 1
> t+2:  43   (… and ends)
> 
> time t+3:  f 42
> t+4:   = 2
> t+5:  44
> 
> Conclusion:  f 42 != f 42
> 
> (This seems so extraordinarily obvious that maybe Heinrich has something else 
> in mind.)
> 
> This seems such an obviously incorrect conclusion.
> 
> f42 is a funtion for returning a program for returning an int, not a function 
> for returning an int.


My conclusion holds:  f 42 != f 42.  Obviously, so I won't burden you with an 
explanation. ;)

-Gregg___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 10:19 AM, Conal Elliott wrote:

> 
> 
> On Fri, Dec 30, 2011 at 12:49 AM, Heinrich Apfelmus 
>  wrote:
> 
> The function
> 
>  f :: Int -> IO Int
>  f x = getAnIntFromTheUser >>= \i -> return (i+x)
> 
> is pure according to the common definition of "pure" in the context of purely 
> functional programming. That's because
> 
>  f 42 = f (43-1) = etc.
> 
> Put differently, the function always returns the same IO action, i.e. the 
> same value (of type  IO Int) when given the same parameter.
> 
> Two questions trouble me:
> 
> How can we know whether this claim is true or not?


time t:  f 42   (computational process implementing func application begins…)
t+1:= 1
t+2:  43   (… and ends)

time t+3:  f 42
t+4:   = 2
t+5:  44

Conclusion:  f 42 != f 42

(This seems so extraordinarily obvious that maybe Heinrich has something else 
in mind.)

-Gregg___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 30, 2011, at 10:34 AM, Artyom Kazak wrote:

> Gregg Reynolds  писал(а) в своём письме Fri, 30 Dec 2011 
> 17:23:20 +0200:
> 
>> Regarding side-effects, they can be (informally) defined pretty simply:  any 
>> non-computational effect caused by a computation is a side-effect.
> 
> I wonder: can writing to memory be called a “computational effect”? If yes, 
> then every computation is impure. If no, then what’s the difference between 
> memory and hard drive?
> 

Great question!  It suggests that the line between computation and its side 
effects is not as clear-cut as we (well, I) thought.

If computations are Platonistic, mathematico-logical "things", then is actual 
computation a side-effect of the Platonic Idea?  Heh heh.

> By the way, the Data.HashTable is in IO monad. Is it impure? Would it be pure 
> if designers had chosen to use ST instead?

Dunno, somebody else will have to answer that one.

-Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 29, 2011, at 2:16 PM, Steve Horne wrote:
> 
> Of course you can extract values out of IO actions to work with them - the 
> bind operator does this for you nicely, providing the value as an argument to 
> the function you pass to the right-hand argument of the bind. But that 
> function returns another IO action anyway - although you've extracted a value 
> out and the value affects a computation, all you can do with it in the long 
> run is return another IO action.
> 
> Even so, that value can only be extracted out at run-time, after the action 
> is executed.
> 
> So, consider the following...
> 
> getAnIntFromTheUser :: IO Int
> 
> From a pure functional point of view, that should return the same action 
> every time. Well, the partially evaluated getAnIntFromTheUser has the same 
> structure each time - but the actual Int packaged inside the action isn't 
> decided until runtime, when the action is executed. At compile-time, that 
> action can only be partially evaluated - the final value OF THE ACTION 
> depends on what Int the user chooses to give because that Int is a part of 
> the action value.

Howdy Steve,

You are correct that Haskell is not, strictly speaking "pure" - no language 
that does anything useful (e.g. IO) can possibly be purely functional.  But 
there seems to be a certain amount of language policing in the "Haskell 
community" - "pure" means what we mean when we use it to describe Haskell, and 
don't you dare use it otherwise.  Ok, but that just leads to riddles like "when 
is a pure language impure?"  A: when it isn't pure.

Several posts to this thread have insisted that IO values are really values 
like any other values, can be reasoned about, etc. and that the process 
yielding the value (including possible side-effects) is therefore irrelevant or 
secondary or etc..  Well, you can reason about them indirectly, by virtue of 
their types, but you can't reason about the values themselves, because they are 
non-deterministic and undecidable.  And the process clearly is relevant, since 
it motivates the use of the value in the first place.  Not much point in a pure 
IO value that does not cause IO, and if the side effects were truly irrelevant 
to the use of such values then we would not need monads to order their 
evaluation.  So the argument that all of Haskell is immaculately, purely 
functional is pure hooey, for me at least.  I completely understand what people 
mean when they talk like this; I just think it's a misuse of English.

Now one way of understanding all this is to say that it implicates the 
static/dynamic (compile-time/run-time) distinction: you don't know what e.g. IO 
values are until runtime, so this distinction is critical to distinguishing 
between pure and impure.  I gather this is your view.

I think that is reasonable, but with the caveat that it must be at the right 
level of abstraction.  I don't think ASTs etc. enter into it - those are 
implementation techniques, and the only generalization we can apply to 
compilers is that they do implement the language definition, not how they do it 
(not all C compilers use ASTs).  The right level of abstraction (IMHO) is the 
distinction between atemporality and temporality.  The functional stuff is 
atemporal, which means among other things that evaluation is unordered 
(evaluation being a temporal process).  Adding IO etc. capabilities to the 
purely functional fragment of a language infects it with temporality.  But we 
can model temporality using order, so we can dispense with the notion of 
run-time and say that IO etc. stuff adds an ordered fragment to the unordered 
fragment.  One goal of the language is then to enforce a strict correspondence 
between the order of events outside the program (e.g. keystrokes) and "events" 
inside the program (getchar).

The beauty of the monad solution is not that it magically transforms 
non-functional stuff like IO into functional stuff, but that it exploits type 
discipline to make such operations *mimic* purely functional stuff in a sense - 
but only at the level of typing.  Impure operations then have purely functional 
type discipline while remaining essentially non-functional.  So I think of 
Haskell as a quasi-pure or hybrid language.  C on the other hand is totally 
impure (except for predefined constants like '1').  For totally pure languages 
you have to look elsewhere, e.g. logics - there are no pure programming 
languages.

It's fairly easy to grasp the point by going back to Turing's original insight. 
 The cornerstone of his ideas was not the machine but the human calculator 
working with pencil and paper, finite memory, etc.  So to see the diff all you 
have to do is think about what a human does with a problem (program) written on 
paper.  Give the human calculator a computable task - add 2+2 - and you can be 
confident you will receive a definite answer in a finite amount of time.  Lard 
this with a non-computable step - add 2 + 2 + getInt - and al

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 29, 2011, at 1:21 PM, Heinrich Apfelmus wrote:

> Why would  IO Int  be something special or mysterious?

I don't know if it is special or mysterious, but I'm pretty sure IO is 
non-deterministic, non-computable, etc.  In other words not the same as 
computation.

> It's an ordinary value like everything else; it's on the same footing as 
> [Char], Maybe Int, Int -> String, Bool, and so on. I see no difference 
> between the list  [1,2,3] :: [Int]  and the action  "pick a random number 
> between 1 and 6" :: IO Int  .

We'll have to agree to disagree - I see a fundamental difference.  But that's 
ok, nothing says everybody has to agree on the One True Way to think about 
computing.

Cheers,

Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 29, 2011, at 12:33 PM, Donn Cave wrote:

> Quoth Gregg Reynolds ,
> ..
>> A minor point maybe, but germane to the original post (I hope).
> 
> It isn't - I mean, I'm not really sure what your point is, but
> the example really returns the same IO value, not just one of
> the same type.
> 
> Consider an example with implementation:
> 
>   wint :: Int -> IO Int
>   wint a = let s = show a in do
>   putStr s
>   return (length s)
> 
> Now the expression "wint 994" is a value of type IO Int, and
> any instance of that expression is the same value

Ok, but if that were all there is to it we would not need monads.  I guess it 
may boil down to a matter of taste in definition and exposition - to me any 
account of stuff like IO Int that omits mention of the fact that, well, IO is 
involved, is incomplete.  But then I like the theoretical and even 
philosophical side of things where others tend to want to get on with writing 
useful code. ;)  And the original post was if I remember about purity/impurity 
etc.

> - an action
> is not the same as the action's result.

Nor is a computation the same as the computation's result.  The critical 
difference is that computations are deterministic processes, and "actions" (IO, 
rand, etc.) are not.  Therefore they are not functions, their evaluation must 
be ordered, and they cannot even in principle be fully modeled in purely 
functional terms.  At least I don't see how they can.

>  You can use this
> value in pure Haskell expressions with confidence.

Because they are monadic, not because they are values like other values.

-Gregg



___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 29, 2011, at 11:29 AM, Antoine Latter wrote:

> On Thu, Dec 29, 2011 at 11:14 AM, Gregg Reynolds  wrote:
>> 
>> On Dec 29, 2011, at 11:01 AM, Iustin Pop wrote:
>> 
>>> And to clarify better my original email: yes, (bar x) always gives you
>>> back the same IO action;
>> 
>> More precisely: the same *type*.
>> 
> 
> I'm confused - what do you mean by "type"? I don't think that Iustin's
> statement needs any sort of qualifier - (bar x) always returns the
> same IO action when called with the same value for x, no matter how
> many times you call it.

Maybe it doesn't need qualification, but my guess is that most people read "IO 
Int" to mean something like "IO action of type int".  But computation does not 
involve "action".  Action is just an explanatory device - a kind of macguffin - 
to help explain what's going on with IO, which is non-computational.  But it is 
a type, and in Haskell it's all about the types.  "IO Int" is a type 
designator, not an action designator.  A minor point maybe, but germane to the 
original post (I hope).

-Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 29, 2011, at 11:01 AM, Iustin Pop wrote:

> On Thu, Dec 29, 2011 at 05:55:24PM +0100, Iustin Pop wrote:
>> On Thu, Dec 29, 2011 at 05:51:57PM +0100, Jerzy Karczmarczuk wrote:
>>> Iustin Pop::
 In practice too:
 
 bar _ = do
   s<- readFile "/tmp/x.txt"
   return (read s)
 
 Once you're in a monad that has 'state', the return value doesn't
 strictly depend anymore on the function arguments.
>>> Nice example. PLEASE, show us the trace of its execution. Then, the
>>> discussion might be more fruitful
>> 
>> Sorry?
>> 
>> I did the same mistake of misreading the grand-parent's "IO Int" vs.
>> "Int", if that's what you're referring to.
>> 
>> Otherwise, I'm confused as what you mean.
> 
> And to clarify better my original email: yes, (bar x) always gives you
> back the same IO action;

More precisely: the same *type*.

> but the results of said IO action are/can be
> different when executed.
> 

-Gregg

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Dec 29, 2011, at 9:16 AM, Donn Cave wrote:

> Quoth Gregg Reynolds ,
>> On Wed, Dec 28, 2011 at 2:44 PM, Heinrich Apfelmus
>>  wrote:
>>> 
>>> The beauty of the IO monad is that it doesn't change anything about purity.
>>> Applying the function
>>> 
>>>  bar :: Int -> IO Int
>>> 
>>> to the value 2 will always give the same result:
>>> 
>>>  bar 2 = bar (1+1) = bar (5-3)
>> 
>> Strictly speaking, that doesn't sound right.
> 
> Look again at the sentence you trimmed off the end:
> 
>>> Of course, the point is that this result is an *IO action* of
>>> type IO Int, it's not the Int you would get "when executing this
>>> action".
> 
> I believe that more or less points to the key to this discussion.
> If it didn't make sense to you, or didn't seem relevant to the
> question of pure functions, then it would be worth while to think
> more about it.

Ok, let's parse it out.  "…it's not the int you would get 'when executing this 
action".  Close, but no cooky: it's not any kind of int at all (try doing 
arithmetic with it).  "IO Int" is a piece of rhetoric for the mental 
convenience of the user; Haskell does not and cannot know what the result of an 
IO action is, because it's outside the scope of the language (and computation). 
 (The "Int" part of "IO Int" refers to the input, not the output; it's just a 
sort of type annotation.)  It's not even a computation, unless you want to take 
a broad view and include oracles, interaction, etc. in your definition of 
computation.

-Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] On the purity of Haskell

[Gregg Reynolds]

On Wed, Dec 28, 2011 at 2:44 PM, Heinrich Apfelmus
 wrote:
>
> The beauty of the IO monad is that it doesn't change anything about purity.
> Applying the function
>
>   bar :: Int -> IO Int
>
> to the value 2 will always give the same result:
>
>   bar 2 = bar (1+1) = bar (5-3)

Strictly speaking, that doesn't sound right.  The "result" of an IO
operation is outside of the control (and semantics) of the Haskell
program, so Haskell has no idea what it will be.  Within the program,
there is no result.  So Int -> IO Int is not really a function - it
does not map a determinate input to a determinate output.  The IO
monad just makes it look and act like a function, sort of, but what it
really does is provide reliable ordering of non-functional operations
- invariant order, not invariant results.

To respond to original post: no language that supports IO can be
purely functional in fact, but with clever design it can mimic a
purely functional language.

Cheers

Gregg

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Category theory as a design tool

[Gregg Reynolds]

On Wed, Jun 22, 2011 at 2:59 PM, Arnaud Bailly wrote:

> Hello Greg and Alexander,
> Thanks for your replies. Funnily, I happen to own the 3 books you
> mentionned :-) My interest in category theory is a long standing affair...
>
> Note that owning a book, having read (most of) it and knowing a theory (or
> at least its principles and main concepts) is really quite a different thing
> from being able to apply it. Although I am certainly able to understand the
> Yoneda lemma, I am certainly unable to


Well, you're way ahead of me.  I don't even "get" adjunctions, to tell you
the truth.  By which I mean that I have no intuition about them; it's not so
hard to understand the formal definition, but it's another thing altogether
to grasp the deep significance.


> recognize the opportunity of using that knowledge to derive some new
> knowledge about something else. And being able to define a topoi is very
> different from being able to construct one or infer one out of a given
> category. This is an actual limitation of myself of course.
>

Indeed.  But I'll bet your next paycheck that eventually CT will replace set
theory as the basic mode of thinking about math, even at elementary levels.
 It just awaits that brilliant writer who can connect the dots
appropriately.


>
> Alexander's advice about using diagrams and simple notations is something I
> often try to do and something which most of the times end in writing a bunch
> of functions and data types in Haskell... What I am really looking for is a
> more systematic way of thinking about systems (or system fragments, or
> components) in a categorical way, perhaps starting with a bunch of arrows in
> some abstract category with objects as components and trying to infer new
> objects out of categorical consturctions which are made possible by the
> current diagrams (eg. what would be a pullback in such a category ? What
> would be its meaning ? Does the question itself have a meaning ?).
>
> Maybe this is really foggy and on the verge to fall into "abstract
> nonsense"...
>
> Long live abstract nonsense!

Completely off topic:  a few months ago I had an idea about using category
theory to provide rigorous semantics for the web (esp. rdf stuff etc.)  I'll
probably never find time to work out the details, but it's a fun exercise in
any case; if you want to mess around with applying CT to the real world
maybe you can coem up with improvements.  See
http://blog.mobileink.com/2011/03/resource-token-exchange.html.  It's a bit
of a mess, and some of it I would radically revise, but it might give you
some ideas, if you're interested in the semantic web thingee.



> Best regards,
> arnaud
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Category theory as a design tool

[Gregg Reynolds]

On Tue, Jun 21, 2011 at 11:30 PM, Arnaud Bailly 
wrote:
> (2nd try, took my gloves off...)
> Hello Café,
> I have been fascinated by Cat. theory for quite a few years now, as
> most people who get close to it I think.
>
> I am a developer, working mostly in Java for my living and dabbling
> with haskell and scala in my spare time and assuming the frustration
> of having to live in an imperative word. More often than not, I find
> myself trying to use constructs from FP in my code, mostly simple
> closures and typical data types (eg. Maybe, Either...). I have read
> with a lot of interest FPS (http://homepages.mcs.vuw.ac.nz/~tk/fps/)
> which exposes  a number of OO patterns inspired by FP.
>
> Are there works/thesis/books/articles/blogs that try to use Cat.
> theory explicitly as a tool/language for designing software (not as an
> underlying formalisation or semantics)? Is the question even
> meaningful?

You might try: Category Theory for Computing
Science (Barr
and Wells)

and Conceptual Mathematics: a first introduction to
categories
 (Lawvere)

"Kinship and Mathematical Categories" (by Lawvere) is also interesting.

-Gregg

>
> Thanks in advance,
> Arnaud
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Python is lazier than Haskell

[Gregg Reynolds]

On Thu, Apr 28, 2011 at 11:38 PM, Ben Lippmeier  wrote:

>
> On 27/04/2011, at 7:30 PM, Henning Thielemann wrote:
>
> >  "If Haskell is great because of its laziness,
> >   then Python must be even greater,
> >   since it is lazy at the type level."
>
> Laziness at the value level causes space leaks, and laziness at the type
> level causes mind leaks. Neither are much fun.
>
> If the designers could find a way to support laziness at the programmer
level I for one would be very grateful.

-G
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] A question about monad based on http://en.wikipedia.org/wiki/Monad_(category_theory)

[Gregg Reynolds]

On Mon, Jan 17, 2011 at 9:46 PM, C K Kashyap  wrote:

>
> I am not able to fully understand how those diagrams translate to haskell -
> I can guess that T^2 -> T referes to things like concat operation but not
> able to relate it to bind.
>
> I found it useful to work out the correspondence between monoids and
monads; lots of introductory texts on CT give the example of the category
Mon so I won't bore you with an account here.  Thinking about monoids and
monads helped me move past element-centric thinking toward the arrow-centric
way of thinking in CT.  In particular it's helpful to work out how the mu
operator of a monad (which composes arrows) is a kind of abstraction of
monoid operators (which combine elements).  What you end up with is the
monad as a device you can use to make non-monoidal things behave like
monoids - closure, associativity, identity.

For bind, google around for Kleisli Category and Kleisli star.  I think of
the latter as a kind of hybrid of a function and a functor, although I'm not
entirely sure that's correct.

-Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Denotational semantics for the lay man.

[Gregg Reynolds]

On Mon, Jan 17, 2011 at 12:55 PM, David Sankel  wrote:

> Hello All,
>
> I've recently had the opportunity to explain in prose what denotational
> semantics are to a person unfamiliar with it. I was trying to get across the
> concept of distilling the essence out of some problem domain. I wasn't able
> to get the idea across so I'm looking for some simple ways to explain it.
>
> Does anyone know of a way to explain what's the meaning and objective of
> "distilling the essence" without introducing more jargon. One thing that
> comes to mind is how Newton's equations for gravity were a distillation of
> the essence of the way things fall.
>

A stick figure as an iconic image of a person serves as a symbol of
"person"; i.e. it denotes person.  It works because of the parts and their
arrangement.  Ditto for mathematical expressions: the whole is equal to the
sum of its parts (and the way they are arranged.)  The individual parts
(e.g. the symbol '3') are not iconic, but  the way the whole system works
corresponds exactly with the way we imagine mathematical objects work.

Google around for "correspondence theory of truth" and you might find some
useful material.

It might be useful to introduce Platonism (see wikipedia.)  Also try boiling
it down to compositionality, substitutability, and equality.

It might also help to draw a contrast with what is not denotational.
 Denotational semantics depends essentially on the fiction of univocality,
namely that every symbol has one delimited meaning: it means what it means,
and nothing else.  But in fact univocality is not possible even in theory;
you cannot circumscribe the the proliferation of meanings.   A simple
example:  2+3 denotes (the same thing as) 5; it may also be taken to denote
a computation that yields 5.  But it does not denote the energy consumed in
carrying out that computation.  A horribly inefficient algorithm may have
the same denotation as a very efficient one.  Another way of putting it is
that denotation is about extensionality to the exclusion of intensional
meanings.  Going beyond extensionality is where Category Theory enters the
picture.

HTH
-Gregg Reynolds
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Lambda Calculus: Bound and Free formal definitions

[Gregg Reynolds]

On Wed, Dec 29, 2010 at 9:22 PM, Mark Spezzano  wrote:

> Duh, Sorry. Yes, there was a typo
>
> the second one should read
>
> If E is a combination E1 E2 then X is bound in E if and only if X is bound
> in E1 or is bound in E2.
>

Seems odd.  I recommend you always work from at least three different texts.
 Here's Hindley and
Seldin
:

"An occurrence of a variable x in a term P is called

   - *bound* if it is in the scope of a \x in P  (NB:  using \ as lambda)
   - *bound and binding* iff it is  the x in \x
   - *free* otherwise"

The tricky question is: bound to what, exactly?

-Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] OT: Monad co-tutorial: the Compilation Monad

[Gregg Reynolds]

This is a little off-topic, since it isn't specifically about Haskell, but
since Haskell is the home of the monad tutorial it isn't completely
irrelevant.  The monad tutorial genre is well-known; it's often written
somebody who has just learned the concept trying to explain it, often in
highly imaginative terms (e.g. "a monad is just like a giant squid, with
special tentacles").  I propose "monad co-tutorial" for attempts, often by
an amateur (e.g. me) to work out how a monad appears in an unexpected place.


In particular, I recently suffered through a few days of learning to deal
with Ant and Maven2, which got me thinking about build systems in general,
which got me thinking about the (meta-)language used in such systems, which
got me thinking about What It's Really All About.

Lo and behold - a monad!  I think, anyway.  The basic idea is that program
texts (source or object code) are to programs as sentences are to
propositions.  Compilation transforms one representation into another.  This
can be viewed in terms of the unit natural transformation of a monad of
transformations over program representations.  The multiplication component
captures the fact that program text transformations can be chained, as in
macro expansion, phased optimization, etc.

I'm not sure if this works, but it fits my somewhat limited idea of monads,
so I wrote an article  about it and I'd
appreciate any corrections.  I expect if it does work somebody has already
done something like it, so I would appreciate any pointers to more info.  My
real goal is to think about better language for software build systems,
since what we have now is pretty weak, in my view.  One thing that follows
from thinking in terms of monads is that we can discard the notion of
dependency of object code of source code in favor of a notion of equivalence
(i.e. unit transform).  My hunch is that thinking along such lines might
lead to an improved metalanguage for build DSLs.

Thanks,

Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] "Haskell is a scripting language inspired by Python."

[Gregg Reynolds]

On Thu, Nov 4, 2010 at 4:48 PM, Richard O'Keefe  wrote:

>
> On 4/11/2010, at 9:08 PM, Stephen Tetley wrote:
> >
> >
> > Did Haskell get significant whitespace from Python - doubtful as
> > Python possibly wasn't visible enough at the time, but you never know.
>
> Python did not originate indentation-based syntax.
> Occam has it too.
> I first came across the idea in a rather old book
> which I *think* was by Reynolds.
>
> I had absolutely nothing to do with it.

However, I must say that it is obvious to anybody properly schooled in
philology and hermeneutics, to say nothing of theology and geometry, that
both Python and Haskell stole their whitespace ideas from the medieval
scribes who invented interword spaces.  As is well known, the reason Roman
computers never caught on is because they didn't use white space in their
programming languages.  For more info, see "Space Between Words; The origins
of silent reading" by Paul Saenger, Stanford U Press, 1997. I'm not joking;
anybody who enjoys thinking about computation will find it very enjoyable.
 It's one of those historical works that makes you realize that what you
thought was trivial (e.g. whitespace) is actually of enormous import.


> > Doesn't COBOL have significant layout anyway as an inspiration to
> > both?
>

> Yes and no.  What it actually has relates strongly to punched cards
> and is more like assemblers of the day.
>
> Columns 1 to 6 were for the sequence number.
> Column 7 is called the indicator area.
> Columns 8 to 11 are "Area A".  Certain structure keywords
> and labels must go in that area.
>  Columns 12 to 72 are "Area B".  Normal statements go in that
> area.  Indentation *within* area B has no significance whatever.
>  Columns 73 to 80 have a name (the Identification Field) but
>

And I thought I was the last mainframer alive!  (I'm sure you'll agree
calling COBOL an "inspiration" of Haskell might be a wee bit of a stretch.)
Anyway, anybody who has ever wondered why 80 cols is a standard width now
knows.

-Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Category Theory woes

[Gregg Reynolds]

On Thu, Feb 18, 2010 at 1:31 PM, Daniel Fischer wrote:

> Am Donnerstag 18 Februar 2010 19:55:31 schrieb Nick Rudnick:
> > Gregg Reynolds wrote:
>


> > -- you agree with me it's far away from every day's common sense, even
> > for a hobby coder?? I mean, this is not «Head first categories», is it?
> > ;-)) With «every day's common sense» I did not mean «a mathematician's
> > every day's common sense», but that of, e.g., a housewife or a child...
>
> Doesn't work. You need a lot of training in abstraction to learn very
> abstract concepts. Joe Sixpack's common sense isn't prepared for that.
>
>
True enough, but I also tend to think that with a little imagination even
many of the most abstract concepts can be illustrated with intuitive,
concrete examples, and it's a fun (to me) challenge to try come up with
them.  For example, associativity can be nicely illustrated in terms of
donning socks and shoes - it's not hard to imagine putting socks into shoes
before putting feet into socks.  A little weird, but easily understandable.
My guess is that with a little effort one could find good concrete examples
of at least category, functor, and natural transformation.  Hmm, how is a
cake-mixer like a cement-mixer?  They're structurally and functionally
isomorphic.  Objects in the category Mixer?


> > > Both have a border, just in different places.
> >
> > Which elements form the border of an open set??
>
> The boundary of an open set is the boundary of its complement.
> The boundary may be empty (happens if and only if the set is simultaneously
> open and closed, "clopen", as some say).
>
> Right, that was what I meant; the point being that "boundary" (or border,
or periphery or whatever) is not sufficient to capture the idea of closed v.
open.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Category Theory woes

[Gregg Reynolds]

On Thu, Feb 18, 2010 at 7:48 AM, Nick Rudnick wrote:

>  IM(H??)O, a really introductive book on category theory still is to be
> written -- if category theory is really that fundamental (what I believe,
> due to its lifting of restrictions usually implicit at 'orthodox maths'),
> than it should find a reflection in our every day's common sense, shouldn't
> it?
>
>
Goldblatt works for me.


>
> * the definition of open/closed sets in topology with the boundary elements
> of a closed set to considerable extent regardable as facing to an «outside»
> (so that reversing these terms could even appear more intuitive, or
> «bordered» instead of closed and «unbordered» instead of open),
>

Both have a border, just in different places.


> As an example, let's play a little:
>
> Arrows: Arrows are more fundamental than objects, in fact, categories may
> be defined with arrows only. Although I like the term arrow (more than
> 'morphism'), I intuitively would find the term «reference» less
> contradictive with the actual intention, as this term
>
> Arrows don't refer.


> Categories: In every day's language, a category is a completely different
> thing, without the least
>

Not necesssarily (for Kantians, Aristoteleans?)  If memory serves, MacLane
says somewhere that he and Eilenberg picked the term "category" as an
explicit play on the same term in philosophy.

In general I find mathematical terminology well-chosen and revealing, if one
takes the trouble to do a little digging.  If you want to know what
terminological chaos really looks like try linguistics.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Category Theory woes

[Gregg Reynolds]

On Tue, Feb 2, 2010 at 5:26 AM, Mark Spezzano
wrote:

> Hi all,
>
> Has anyone else found it frustratingly difficult to find details on
> easy-to-diget material on Category theory. The Chapter that I'm stuck on is
> actually labeled Preliminaries and so I reason that if I can't
>

I've looked through at least a dozen.  For neophytes, the best of the bunch
BY FAR is Goldblatt, Topoi: the categorial analysis of
logic.
 Don't be put off by the title.  He not only explains the stuff, but
he
explains the problems that motivated the invention of the stuff.  He doesn't
cover monads, but he covers all the basics very clearly, so once you've got
that down you can move to another author for monads.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Linguistic hair-splitting

[Gregg Reynolds]

On Sat, Jan 30, 2010 at 1:24 AM, Conal Elliott  wrote:

> I call it "an m" or (more specifically) "an Int m" or "a list of Int".  For
> instance, "a list" or "an Int list" or "a list of Int".  - Conal
>
>
> On Wed, Jan 27, 2010 at 12:14 PM, Luke Palmer  wrote:
>
>> On Wed, Jan 27, 2010 at 11:39 AM, Jochem Berndsen 
>> wrote:
>> >> Now, here's the question: Is is correct to say that [3, 5, 8] is a
>> >> monad?
>> >
>> > In what sense would this be a monad? I don't quite get your question.
>>
>> I think the question is this:  if m is a monad, then what do you call
>> a thing of type m Int, or m Whatever.
>>
>> Luke
>>
>
Conal's is the most sensible approach - "what do you call it" amounts to
"what sort of a thing is it", and the best we can say in that respect is
"er, its a thing of type m Whatever".  (My preference, if maximal
explicitness is needed, is to say "it's a token of its type"; some say "term
of type m Whatever".)  Trying to classify such a thing as "value", "object",
"computation", "reduction" etc. inevitably (and necessarily) leads to
tail-chasing since those notions are all essentially equivalent.  Plus they
miss the essential point, which is the typing.

Original poster would probably find Martin-Lof's philosophically-tinged
writings very good on this - clear, reasonably simple, and revelatory, if
you've never closely looked at intuitionistic logic before.  Truth of a
proposition, evidence of a judgment, validity of a
proofis especially readable, as is
On
the meanings of the Logical Constants and the Justifications of the Logical
Laws .
Presents a completely new (to me) way of thinking about "what is it,
really?" questions about computation, monads, etc., i.e. ask not "what is
it?" but "how do you know?" or even "how do you make it?"  The Stanford
article on types and
tokensis also very
enlightening in this respect.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] consulting and contracting

[Gregg Reynolds]

On Tue, Dec 15, 2009 at 3:19 PM, Anton van Straaten
wrote:

>
> Without that advocacy, this client would have used Java by default.  As it
> was, the first of
>
>
I'd be interested in how you pulled that off.  Enlightened client, or slick
sales pitch? Where I work I would consider it a minor miracle just to get
people to consider using a wiki for collaboration.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Why?

[Gregg Reynolds]

On Thu, Dec 10, 2009 at 11:16 AM, John D. Earle  wrote:

>  Dear Gregg,
>
> You wrote, "Just think about how one reads a mathematical text - you need
> not actually compute subformulae or even analyze them logically in order to
> work with them." I hate to have to say this, but do you realize that algebra
> is concerned with functions among other things and it is the fact that these
> expressions are functions and not that they are algebraic that gives them
> this property?
>

Hi John,

I'd say algebra is mostly concerned with equalities and substitutions and
doesn't much care about functions.  The equation for a circle is not a
function but that doesn't mean we can't use algebra to manipulate it.
Algebras might use the concept of function but they are not necessarily
_about_ functions.  One could even argue that the lambda calculus isn't
"about" functions - it's just a calculus, after all.  Haskell goes by the
rules of that calculus; whether the expressions involved denote functions is
not relevant.  The computer is just performs symbol calculus.  Generally all
formal semantics can be reduced to syntactic calculus as far as I can see.


> Functional programming is not a misnomer. It is called functional
> programming because you are quite literally working with functions.
>

Except when you're not.  IO operations are never functions, for example, so
IO expressions never denote functions.  FP languages do not (and cannot)
eliminate the side effectful nature of such operations; the best they can do
is what Haskell does, namely circumscribe them so that they are well-behaved
and thus can be properly managed (algebraically).  But that doesn't make
them functions.  So for me at least "algebraic" better describes how Haskell
works; what you're working with is expressions and you reason about them
algebraically.   You can do this reliably not because everything is a
function but because non-functions are well-behaved.


> Functions have a profound simplifying effect.
>

No argument there.  But the expressive power that comes with first-class
functions is not what distinguishes Haskell et al. - lots of non-FP
languages support them these days.

> The truth is as Haskell has demonstrated that much of the complexity in
> computer programming is artificial and doesn't need to be there. It makes
> having to prove correctness a lot easier, but that is not the only
> motivation behind Haskell and other functional programming languages. The
> push has been getting performance up to a point where the language may be
> regarded as respectable.
>

Sure, but that's only possible because the properties of programs are
provable, which is what makes it possible to reliably transform a program
into an equivalent but more efficient form.

-Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Why?

[Gregg Reynolds]

On Thu, Dec 10, 2009 at 9:13 AM, John D. Earle  wrote:

> Most of the discussion centers on the benefits of functional programming
> and laziness. Haskell is not merely a lazy functional language. It is a pure
> lazy functional language. I may need to explain what laziness is. Laziness
> is where you work through the logic in its entirely before acting on the
> result. In strict evaluation the logic is worked out in parallel with
> execution which doesn't make complete sense, but it does allow for an
> architecture that is close to the machine.
>
>
Just to roil the waters a bit: no programming language can ever hope to be
"purely functional", for the simple reason that real computation (i.e.
computation involving IO, interactivity) cannot be functional.  "Functional
programming" is an unfortunate misnomer.  On the other hand, languages can
be algebraic.  The whole point is provability, not function-ness.

More generally:  judging by the many competing proposals addressing the
issue of how to think formally about real computation (just google stuff
like hypercomputation, interactive computation, etc.; Jack
Copelandhas
lots of interesting stuff on this) is still an open question.  Soare
has
three essential papers
on the subject.
I guess the moral of the story is that the concepts and the
terminology are both still unstable, so lots of terms in common use are
rather ill-defined and misleading (e.g. functional programming).

Lazyness is just a matter of how one attaches an actual computation to an
expression; a better term would be something like "delayed evaluation" or
"just-in-time computation".  You don't have to work through any logic to
have laziness.  Just think about how one reads a mathematical text - you
need not actually compute subformulae or even analyze them logically in
order to work with them.  This applies right down to expressions like "2+3"
- one probably would compute "5" on reading that, but what about
"12324/8353"?  You'd leave the computation until you absolutely had to do it
- i.e. one would probably try to eliminate it algebraically first.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] seems like I'm on the wrong track

[Gregg Reynolds]

On Tue, Dec 1, 2009 at 7:55 PM, Michael Mossey 
wrote:
> Thanks for the reply. Was there something specific you were referring to,
or

Maybe http://plucky.cs.yale.edu/cs431/reading.htm Chapter 9 "An Algebra of
Music."
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] seems like I'm on the wrong track

[Gregg Reynolds]

On Tue, Dec 1, 2009 at 7:01 PM, Michael P Mossey  
wrote:
> Perhaps someone could either (1) help me do what I'm trying to do, or (2)
> show me a better way.
>>
> In this one example, in a OO way of thinking, I have data called
> AssignedNumbers that assigns integers to unique strings and keeps track of
> the used integers and next available integer (the choice of available
> integer could follow a number of conventions so I wanted to hide that in an
> ADT.) So it has an associated function:
>

What do the numbers and strings mean?  Can you use an algebraic type
instead of strings?  Do particular numbers have meaning or are they
just serial numbers?  Can you compute some sort of checksum for the
strings rather than rely on an external list of numbers?  If you must
have a list of numbers, can you embed it in a specialized string type,
so that numbers get assigned as a side-effect of string construction?
In other words, would it help to think more in terms of specific types
rather than generic numbers and strings?

-G
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] I miss OO

[Gregg Reynolds]

On Thu, Nov 26, 2009 at 6:44 AM, Stephen Tetley
 wrote:
> 2009/11/26 Gregg Reynolds :
>
>> Modeling musical stuff could provide an excellent illustration of the
>> difference between OO and the Haskell way; it's the difference between
>> metaphysical engineering and constructive mathematics.
>
>
> Hmm, Stephen Travis Pope's SmOKe - a design that has been the basis of
> various state-of-the-art Smalltalk music systems - seems pretty
> concrete to me rather than metaphysical.
>
> http://heaveneverywhere.com/stp/PostScript/icmc.94.mode.pdf
>

Looks interesting, but what I was trying to get at - ``metaphysical
engineering'' just popped into my head and sounded kinda cool so I
went with it - is that these are two radically different ways of
thinking about what we're doing when we write programs.

For example, Pope talks about music in terms of properties, but then
says "[t]hese properties may be music-specific _objects_ (such as
pitches or spatial positions)..." (emphasis added).  This is standard
OO-speak; there's nothing wrong with it, the point is just that the
domain of interest is viewed as a collection of ``objects'' and their
behaviors, where ``object'' is the word we use for lack of a better
term to refer to things that exist - hence metaphysics.  Are there
_really_ any objects involved, especially where properties are
concerned?  Not for me, though others may differ.  In any case, the
overall picture is that programs are combinations of such objects, so
the program is viewed as the description of a kind of machine - hence
engineering.  In order to describe music, the programmer describes a
machine.

By contrast, a ``purely functional'' approach (I prefer ``algebraic''
as more accurate or at least more revealing) might construe such
properties in terms of  types and operations on values of the types,
which capture the notion of property directly without implicating
objects in any way.  A music library would be viewed in terms of a
language (algebra), with customized names for domain-specific types
and operations, that the programmer can use to describe music instead
of describing a machine that produces music.  Which makes the
programmer a litterateur rather than a constructor of machines, among
other things.

Cheers,

Gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] I miss OO

[Gregg Reynolds]

On Wed, Nov 25, 2009 at 2:51 PM, Michael Mossey  wrote:
>
> So if I have objects/data note1, cursor1, and staff1,
>
> Python:
>  note1.time()
>  cursor1.time()
>  staff1.time()
>
> Haskell needs something like
>  note_time note1
>  cursor_time cursor1
>  staff_time staff1

Modeling musical stuff could provide an excellent illustration of the
difference between OO and the Haskell way; it's the difference between
metaphysical engineering and constructive mathematics. Think algebra.
Haskell isn't just about types, its about algebraic types: structures
and operations (signatures).  So instead of asking ``what kind of
object is a note?'', ask ``what is the algebra of notes?''  And not
``what kind of mathematical object is a note?'' but ``what kind of
alegebraic formula describes (constructs) a note?''  You get a type
constructor and some data constructors, which are essentially
algebraic formulae that allow you to construct (i.e. refer to,
describe) note values using values of other types.  Then you add some
operators, which are defined using those constructive formulae
(deconstruction via pattern matching.)  Type classing allows you to
use the same names for operations on different algebras.  Etc.

Then ``how do I access the time contained in this note?" becomes ``how
do I construct a formula describing the time value used to construct
this note?''.  I.e. it's all about the algebraic notations rather than
the metaphysics of ``objects'', and Haskell gives you a variety of
ways to do this, as other responses in the thread have pointed out.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] I miss OO

[Gregg Reynolds]

On Thu, Nov 26, 2009 at 1:50 AM, Eugene Kirpichov  wrote:
>
> I argue that in the situation you provided, the pitch, duration,
> timbre and instrument are "essential" attributes of the dot, whereas
> time is the position of the dot on paper and should be separated from
> its essence.

`Timing', maybe, or temporal `position', `locus', etc., although
position also applies to pitch (as interval).  Anything but `time',
which is guaranteed to induce confusion.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] What *is* a DSL?

[Gregg Reynolds]

On Thu, Oct 8, 2009 at 6:08 AM, Colin Paul Adams
wrote:

> > "George" == George Pollard  writes:
>
>George> I'd also like to note that the canonical pronunciation of
>George> DSL ends in "-izzle".
>
> Whose canon?
>
> Interestingly, I have always assumed the canonical pronunciation of
> DSSSL was diesel, as JADE stands for JAmes's DSSSL Engine.
>
> I don't see why removing extra S-es should shorten the vowel.
>
>  Wht vwl?  U mst b Englsh. 2 n Amrcn, DSSSL is "dissel"; all short vowels.
DSL is "dee-ess-ell".  "Dizzle" is a brbrzm.


-grgg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] commending "Design concepts in programming languages"

[Gregg Reynolds]

On Tue, May 12, 2009 at 1:04 PM, Max Rabkin  wrote:
> On Tue, May 12, 2009 at 1:41 PM, Wolfgang Jeltsch
>  wrote:
>> At least, I cannot
>> remember seeing the other notation (first morphism on the left) in
category
>> theory literature so far. It’s just that my above-mentioned professor
told me
>> that category theorists would use the first-morphism-on-the-left
notation.
>
> I've seen the notation f;g for g.f somewhere (and Wikipedia mentions
> it). I think it's less ambiguous than just fg (which I've seen for f.g
> too), but in Haskell we have the option of >>>. A flipped application
> might be nice to go with it. How about >$> ?

FYI:

Unicode U+2A3E  Zed notation relational composition (small circle over a 9)

Examples at http://staff.washington.edu/jon/z/toolkit.html#pair3
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Referential Transparency and Monads

[Gregg Reynolds]

On Thu, Apr 9, 2009 at 11:46 PM, Brandon S. Allbery KF8NH
 wrote:
>
> I still don't understand this; we are passing a World and getting a World
> back, *conceptually* the returned World is modified by putStr.  It's not in
> reality, but we get the same effects if we write to a buffer and observe
> that buffer with a debugger --- state threading constrains the program to
> the rules that must be followed for ordered I/O, which is what matters.
>

You might find it useful to back up and think about the nature of
computation.  I did, anyway, when I was slogging through this stuff.
Computability is all based on intuition about the *process* of
calculating (see section 9 I think it is of Turing's original paper).
IO "operations" - whatever one calls them - are by definition not
computable.  "Referentially transparent IO expressions" is an
oxymoron, since the operations involved do not (cannot) correspond to
any process that corresponds intuitively to computation and thus
cannot refer transparently.  So (going back to your original question)
we can never get RT, but we can get the next best thing, which is
manageability, which is what monads and other IO techniques are all
about.

YMMV, but for me the IO-as-state-transformer-operating-on-World is
quite misleading.  It's one possible method for dealing with IO
conceptually but it's easy to get the incorrect impression that IO
*is* some kind of state transformation, when in fact there is no
essential connection between the two.  There is no "state" nor
"transformation" involved; an IO expression just references the result
of some indeterminate non-computing process, just like a referentially
transparent expression like '3+2' references the result of a
determinate computing process.  Monads etc. just allow us to use IO
expressions as if they were computable even though they're not, by
enforcing sequencing.  Or to put it another way, what really counts is
predictability, not referential transparency.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] [SoC] XML Schema Implementation

[Gregg Reynolds]

On Mon, Mar 30, 2009 at 5:16 PM, Vlad Dogaru  wrote:
> Hello everyone,
>
> I am writing to judge interest in a Summer of Code proposition: an XML
> Schema[1] implementation, described as a possbile application here[2].
> As both a tool and an inspiration, I intend to use HaXML[3].
>
> More specifically, I would be interested in the degree the Haskell
> community uses XML Schema, and if you were tempted to use it if we had
> an implementation. To further expand the question, how useful do you
> consider each of these components:
>  * a validator
>  * a pretty-printer
>  * a translator from XML Schema to Haskell, similar to DtdToHaskell[4]

A RelaxNG <-> XML Schema translator would be very useful.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] about Haskell code written to be "too smart"

[Gregg Reynolds]

2009/3/25 Zachary Turner :
>
> On the other hand, -certain- languages are more expressive than others.  As
> an example, I personally find English far more expressive than both
> Vietnamese and Japanese, yet English is far more complicated.  Japanese, for

Way off topic, but for what it's worth, you can take it as axiomatic
that all natural languages are equally expressive, qua languages.
They're also equally easy/hard overall.  The areas of difficulty are
just in different places.  Japanese grammar is extraordinarily simple,
but achieving mastery of the spoken language *in Japanese society* is
next to impossible, because usage reflects social constructions.  As
you no doubt know, what is not said is sometimes just as expressive as
what is said in Japanese; very maddening to a logorrheic American,
just as an English speaker's need to explicitly articulate
*everything* is no doubt annoying to Japanese.

Regarding spelling and phonology: the idea that "one symbol, one
sound" is somehow optimal is the Myth That Will Not Die.  None other
than Chomsky himself argued that English orthography is near-optimal
for the English language.  All writing systems are designed to serve
speakers of the language, and many languages are poorly modeled by a
one symbol, one sound system.

I'm not sure there's a lesson there for formal language designers and
programmers, except maybe that the expressiveness (elegance?) of a
text usually depends to a great extent on the writer more than the
language.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] about Haskell code written to be "too smart"

[Gregg Reynolds]

On Tue, Mar 24, 2009 at 12:41 PM, Manlio Perillo
 wrote:

> I too have this feeling, from time to time.
>
So do I, because I haven't had the time to learn what I need to learn
in order to read the code smoothly.  I find that when I do work out
the meaning, most often the style reflects conciseness or
expressiveness, not obfuscatory tricks that the language allows.
>
> Since someone is starting to write the Haskell coding style, I really
> suggest him to take this "problem" into strong consideration.

Rule One of the Haskell Coding Style Handbook:  learn Haskell first,
then worry about style.  After all, nobody in her right mind would
tackle a French style manual without learning French first.  Although
I suppose one could argue that learning Haskell in fact involves
learning various styles.  ;)

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] about Haskell code written to be "too smart"

[Gregg Reynolds]

On Tue, Mar 24, 2009 at 1:42 PM, Manlio Perillo
 wrote:
>
> But, as an example, when you read a function like:
>
> buildPartitions xs ns = zipWith take ns . init $ scanl (flip drop) xs ns
>
> that can be rewritten (argument reversed) as:
>
> takeList :: [Int] -> [a] -> [[a]]
> takeList [] _         =  []
> takeList _ []         =  []
> takeList (n : ns) xs  =  head : takeList ns tail
>    where (head, tail) = splitAt n xs
>
> I think that there is a problem.

This crops up all the time even in simple mathematics.  One way to
provide assistance to newcomers is to provide a quasi-English reading
of the notation.  Take as an example a simple set comprehension
expression (using Z email notation,
http://csci.csusb.edu/dick/samples/z.lexis.html):

   { x : Int | 0 < x < 10 /\ x %e Odd @ 2*x }

That's pretty opaque for beginners until they learn to read | as "such
that", %e as "member of" and @ as "generate", so that they can express
the idea in quasi-English:  "form a set by taking  all integers x such
that ... and ..., then generate the result by doubling them" or the
like.  Or take | as "filter" and @ as "map"; the point is it helps to
be able to express it in something like natural language.

Do something similar for your buildPartitions definition and I'll bet
you'll end up with something much more user friendly than takeList.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: categories and monoids

[Gregg Reynolds]

On Thu, Mar 19, 2009 at 5:43 AM, Wolfgang Jeltsch
 wrote:
> Am Mittwoch, 18. März 2009 15:17 schrieben Sie:
>> Wolfgang Jeltsch schrieb:
>> > Okay. Well, a monoid with many objects isn’t a monoid anymore since a
>> > monoid has only one object. It’s the same as with: “A ring is a field
>> > whose multiplication has no inverse.” One usually knows what is meant
>> > with this but it’s actually wrong. Wrong for two reasons: First, because
>> > the multiplication of a field has an inverse. Second, because the
>> > multiplication of a ring is not forced to have no inverse but may have
>> > one.
>>
>> “A ring is like a field, but without a multiplicative inverse” is, in my
>> eyes, an acceptable formulation. We just have to agree that “without”
>> here refers to the definition, rather than to the definitum.
>
> Note that you said: “A ring is *like* a field.”, not “A ring is a field.”
> which was the formulation, I criticized above.
>

"Alternatively, the fundamental notion of category theory is that of a
monoid ... a category itself can be regarded as a sort of generalized
monoid."

   --  Saunders MacLane, "Categories for the Working Mathematician"  (preface)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Design Patterns by Gamma or equivalent

[Gregg Reynolds]

2009/3/11 Mark Spezzano :
> I’m very familiar with the concept of Design Patterns for OOP in Java and
> C++. They’re basically a way of fitting components of a program so that
> objects/classes fit together nicely like Lego blocks and it’s useful because
> it also provides a common “language” to talk about concepts, like Abstract
> Factory, or an Observer to other programmers. In this way one programmer can
> instantly get a feel what another programmer is talking about even though
> the concepts are fundamentally abstract.
>
> Because Haskell is not OO, it is functional, I was wondering if there is
> some kind of analogous “design pattern”/”template” type concept that
> describe commonly used functions that can be “factored out” in a general
> sense to provide the same kind of usefulness that Design Patterns do for
> OOP. Basically I’m asking if there are any kinds of “common denominator”
>  function compositions that are used again and again to solve problems. If
> so, what are they called?
>

You might find it useful to read the original works upon which the
whole "design pattern" economy is based, namely Christopher
Alexander's books
(http://www.patternlanguage.com/leveltwo/booksframe.htm?/leveltwo/../bookstore/bookstore.htm).
 I liked "Notes on the Synthesis of Form", which predates his pattern
language stuff.

My $0.02:  design patterns became popular in the imperative language
community precisely because such languages lack the formal discipline
of functional languages.  Alexander came up with the notion of a
pattern language in order to bring some kind of discipline and
abstraction to observed regularities in architecture, urban design,
etc.  By definition such a language cannot have anything close to
formal semantics, any more than a natural language lexicon can have
formal semantics.  Alexander's writing is very interesting and thought
provoking, but I'm not sure it has much to offer the world of
functional programming.

Programmers used Alexander's ideas to try to bring some order to both
specifications and programs.  A pattern language is a natural for
trying to describe a real-world problem one is trying to solve.
Imperative programmers also used it to describe programming patterns.
Implementations of things like Observer/VIsitor etc. are ad-hoc,
informal constructions; the equivalent in a functional language is a
mathematical structure (feel free to fix my terminology).  I don't
think one needs design patterns for Haskell; it has mathematics and
more-or-less formal semantics.  Who needs "Visitor" when you have "For
All"?  Although design patterns may still be useful for describing a
real-world problems I suspect one would be better off dumping the
notion of design pattern, the better to avoid cognitive dissonance
when trying to think in purely functional terms.

Cheers,
-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Against cuteness

[Gregg Reynolds]

On Thu, Mar 12, 2009 at 9:17 PM, Benjamin L. Russell
 wrote:
> On Thu, 12 Mar 2009 09:11:15 -0500, Gregg Reynolds 
> wrote:
>
>>I don't think so.  Bad design will lose them (and many others), but
>>good design and cuteness are two different things.
>
> It's also possible for a good design to be cute, too.
>

De cutibus non est disputandem.

Personally I think something interesting could be done with Thoth
(nice open svg image at http://en.wikipedia.org/wiki/Thoth):  God of
reading/writing, math.  When conflated with Hermes, also of
boundaries, thieves and scoundrels, etc.

Then there's Haskell B. Curry himself; notice the resemblance
(http://www.haskell.org/bio.html) with J. R. "Bob" Dobbs
(http://en.wikipedia.org/wiki/J._R._%22Bob%22_Dobbs).  An artist could
"comicize" an image of Curry.  Then it's only a short step to actual
cultdom - why stop with a mere web community when you can legally
establish a religious cult and actually ordain Ministers?
(http://www.subgenius.com/scatalog/membership.htm).

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Against cuteness

[Gregg Reynolds]

On Thu, Mar 12, 2009 at 7:07 AM, Benjamin L. Russell
 wrote:
>
> Here, there are a lot of Japanese Haskell fans who love the beauty of
> Haskell, and you will risk losing a lot of them if you choose a mascot
> without any cuteness factor.  A lot of my friends meet together every

I don't think so.  Bad design will lose them (and many others), but
good design and cuteness are two different things.

>
> You can still distinguish yourself from O'Reilly without losing the
> cuteness factor with a logo like one of the following:
>

We must have vastly different ideas of cute.  I don't consider those
examples cute.  How about this as a criterion:  if it makes 13-year
old Japanese girls squeal "kawa!" then it's too cute.  Also if it
involves the color pink.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] monadic logo

[Gregg Reynolds]

At risk of becoming the most hated man in all Haskelldom, I'd like to
suggest that the Haskell logo not use lambda symbols.  Or at least not as
the central element.  Sorry, I know I'm late to the party, but the thing is
there is nothing distinctive about lambda; it's common to all FPLs.
Besides, Lisp/Scheme already have that franchise.

What is distinctive about Haskell it's use of the monad.  The Pythagorean
monad symbol is wonderfully simple:

http://en.wikipedia.org/wiki/Monad_(Greek_philosophy).
Something might also be done with the triad to reflect the fact that the
monad in cat theory is actually a triple (
http://en.wikipedia.org/wiki/Triad_(Greek_philosophy)
).

The "Cup or Monad" (http://www.sacred-texts.com/chr/herm/hermes4.htm), with
a little bit of work, could be turned into an amusing Haskell manifesto.
Lots of interesting imagery from the gnostic tradition (
http://www.sacred-texts.com/gno/th2/index.htm), although SICP seems already
to have  used something similar (
http://mitpress.mit.edu/images/products/books/0262011530-f30.jpg).  Hermes
Trismegistus = Thrice-great Hermes -> Haskell Trismegistus, Thrice-Glorious
Haskell, etc.  Might be too cute.

There's also Leibniz' monadology - I can't think of any visual imagery to go
with it, but he did end up with the "best of all possible worlds"
hypothesis, which gives us a slogan sure to irritate:  "Haskell - the best
of all possible languages".  Not to mention "Haskell Monadology" as a name
for the official Haskell definition, etc.

Hey, at least it isn't cute.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Against cuteness

[Gregg Reynolds]

On Wed, Mar 11, 2009 at 5:25 AM, Bulat Ziganshin
wrote:

> Hello Gregg,
>
> Wednesday, March 11, 2009, 1:17:41 PM, you wrote:
>
> > are not O'Reilly.  Of all the billions of images from all the
> > cultures in the world available to us we can surely find something
> > that is witty or charming without being cute.
>
> it will not be fun :)
>

Perhaps not, but it also won't be torture.  I can't take any more cuteness.
;)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Against cuteness

[Gregg Reynolds]

Regarding logos/mascots:  nothing personal folks, but I would like to cast a
loud firm vote against all forms of cuteness, especially small furry animal
cuteness.  It's been done half to death, and we are not O'Reilly.  Of all
the billions of images from all the cultures in the world available to us we
can surely find something that is witty or charming without being cute.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: [Haskell] Lazy IO breaks purity

[Gregg Reynolds]

On Thu, Mar 5, 2009 at 7:08 AM, Simon Marlow  wrote:

>
> So the argument is something like: we can think of the result of a call to
> unsafeInterleaveIO as having been chosen at the time we called
> unsafeInterleaveIO, rather than when its result is actually evaluated. This
> is on dodgy ground, IMO: either you admit that the IO monad contains an
> Oracle, or you admit it can time-travel.   I don't believe in either of
> those things :-)
>
>
Surely there's a quantum mechanical metaphor waiting to happen here.

   getCat ::  IO Cat

If "getCat" appears in a program text, does it denote or not?  Or both?  If
it does, is the cat alive or dead? (Apologies to
Schrodinger).


-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: Paper draft: "Denotational design with type class morphisms"

[Gregg Reynolds]

On Fri, Feb 20, 2009 at 9:12 AM, Achim Schneider  wrote:

> Robin Green  wrote:
>
> > On Fri, 20 Feb 2009 15:17:14 +0100
> > Achim Schneider  wrote:
> >
> > > Conal Elliott  wrote:
> > >
> > > > DRAFT version ___ comments please
> > > >
> > > Conal, please, PLEASE, never, EVER again use the word "meaning" if
> > > you actually mean "denotation". It confuses the hell out of me,
> > > especially the (I guess unintended) connotation that you analyse
> > > the meaning of a particular instance's existence on a cosmic scale.
> >
> > It shouldn't confuse you. Using "means" for "denotes", and likewise
> > "meaning" for "denotation", is correct English, and very common usage
> > too.
> >
> (length . denotations) "to mean" > (length . denotations) "to denote"
>
> (read: "to denote" is more defined than "to mean")
>
> Following your argument through, we should talk kinda like "hey, we do
> something with that thingy to do that-other thingy to that thingy
> over there". 99% of my former teachers would tear you to shreds... in
> mid-air (during lift-off).
>
> I can't talk about the whole of English usage, but I never saw
> "meaning" in a mathematical context where "denotation" would work, too,
> except in Conal's writings.
>
>
> ...and that doesn't even include that my native language isn't English
> but German, in which "to mean" nounificates using another object:
> It translates to "Opinion" instead of "Denotation".
> "deuten" (to intepret, to point) is a very well-defined concept in
> German and doesn't like to be messed with.
>

The distinction is very clear in technical English but often disregarded in
ordinary speech.  http://consc.net/papers/intension.html is very
informative.

-gregg, your faithful half-baked philosophaster
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How to create an online poll

[Gregg Reynolds]

2009/2/19 Luke Palmer 

> 2009/2/19 Rick R 
>
>> I think the capabilities community including E and Coyotos/BitC have
>> extensively addressed this topic. Coyotos is taking the correct approach for
>> trusted voting platform. Since, even if your software is trustworthy, it
>> can't be trusted if the OS on which it runs is suspect.
>
>
> Woah, that's a pretty interesting question!  How do you write software
> which is protected against a malicious operating system (mind -- not
> erroneous, but rather somebody detecting the software you're running and
> changing your vote).  Maybe some sort of randomized cryptographic technique,
> in which, with high probability, the OS either runs your program correctly
> or causes it to crash.
>
> It gets worse.  Even if you write your OS in Haskell, how do you know your
compiler hasn't been compromised?  Or the hardware?  The solution
necessarily involves a social component, e.g. Haskell, with the development
practices of OpenBSD (continuous re-auditing of everything including tools,
complete openness, etc.)  IOW, it'll never happen, but it might end up
better than paper ballots.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How to create an online poll

[gregg reynolds]

Perhaps you are a subversive functor,  hmm?  We have monadic ways of conrolling 
you, fiend!  Tellus who your natural tansformations are, or else!

Andrew Wagner  wrote:

>Help! Help! I'm being suppressed!!
>
>On Feb 18, 2009, at 5:05 PM, Rick R  wrote:
>
>> I can't comment on any quantitative side effects, but the some  
>> intangible side effects include Distrustful Populace and  
>> MaliciousDissenters. However, if ghc is run with the - 
>> XUnscrupulousPolitics  flag, those can be suppressed.
>>
>> On Wed, Feb 18, 2009 at 4:33 PM, gregg reynolds   
>> wrote:
>> I.e. war, plague.famine. etc.
>>
>> gregg reynolds  wrote:
>>
>> >But what about the side effects?
>> >
>> >Rick R  wrote:
>> >
>> >>I'm sure Premier Election Solutions (formerly Diebold) can provide  
>> us with
>> >>an online voting solution.
>> >>Their value-add services allows us to set the outcome beforehand,  
>> so, in
>> >>effect, the the voting process will be determinate. Which is  
>> certainly of
>> >>interest to Haskell coders.
>> >>
>> >>
>> >>On Wed, Feb 18, 2009 at 4:05 PM, Max Rabkin   
>> wrote:
>> >>
>> >>> On Wed, Feb 18, 2009 at 10:40 PM, Anton van Straaten
>> >>>  wrote:
>> >>> > There's also the Condorcet Internet Voting Service:
>> >>> >
>> >>> >  http://www.cs.cornell.edu/andru/civs.html
>> >>>
>> >>> This looks like exactly what we need! Any objections?
>> >>>
>> >>> --Max
>> >>> ___
>> >>> Haskell-Cafe mailing list
>> >>> Haskell-Cafe@haskell.org
>> >>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >>>
>> >>
>> >>
>> >>
>> >>--
>> >>We can't solve problems by using the same kind of thinking we used  
>> when we
>> >>created them.
>> >>   - A. Einstein
>> >>___
>> >>Haskell-Cafe mailing list
>> >>Haskell-Cafe@haskell.org
>> >>http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
>>
>> -- 
>> We can't solve problems by using the same kind of thinking we used  
>> when we created them.
>>- A. Einstein
>> ___
>> Haskell-Cafe mailing list
>> Haskell-Cafe@haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How to create an online poll

[gregg reynolds]

Ok, that might protect us against the 7 plagues, so I'm not so worried about 
locusts.  But what about Java, PHP etc.  Is the monad sufficient protection 
against ultra-supernatural evil?

Andrew Wagner  wrote:

>Just wrap it in a ReallySafeWePromiseMonad
>
>2009/2/18 gregg reynolds 
>
>> I.e. war, plague.famine. etc.
>>
>> gregg reynolds  wrote:
>>
>> >But what about the side effects?
>> >
>> >Rick R  wrote:
>> >
>> >>I'm sure Premier Election Solutions (formerly Diebold) can provide us
>> with
>> >>an online voting solution.
>> >>Their value-add services allows us to set the outcome beforehand, so, in
>> >>effect, the the voting process will be determinate. Which is certainly of
>> >>interest to Haskell coders.
>> >>
>> >>
>> >>On Wed, Feb 18, 2009 at 4:05 PM, Max Rabkin 
>> wrote:
>> >>
>> >>> On Wed, Feb 18, 2009 at 10:40 PM, Anton van Straaten
>> >>>  wrote:
>> >>> > There's also the Condorcet Internet Voting Service:
>> >>> >
>> >>> >  http://www.cs.cornell.edu/andru/civs.html
>> >>>
>> >>> This looks like exactly what we need! Any objections?
>> >>>
>> >>> --Max
>> >>> ___
>> >>> Haskell-Cafe mailing list
>> >>> Haskell-Cafe@haskell.org
>> >>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>> >>>
>> >>
>> >>
>> >>
>> >>--
>> >>We can't solve problems by using the same kind of thinking we used when
>> we
>> >>created them.
>> >>   - A. Einstein
>> >>___
>> >>Haskell-Cafe mailing list
>> >>Haskell-Cafe@haskell.org
>> >>http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>> ___
>> Haskell-Cafe mailing list
>> Haskell-Cafe@haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How to create an online poll

[gregg reynolds]

I.e. war, plague.famine. etc.

gregg reynolds  wrote:

>But what about the side effects?
>
>Rick R  wrote:
>
>>I'm sure Premier Election Solutions (formerly Diebold) can provide us with
>>an online voting solution.
>>Their value-add services allows us to set the outcome beforehand, so, in
>>effect, the the voting process will be determinate. Which is certainly of
>>interest to Haskell coders.
>>
>>
>>On Wed, Feb 18, 2009 at 4:05 PM, Max Rabkin  wrote:
>>
>>> On Wed, Feb 18, 2009 at 10:40 PM, Anton van Straaten
>>>  wrote:
>>> > There's also the Condorcet Internet Voting Service:
>>> >
>>> >  http://www.cs.cornell.edu/andru/civs.html
>>>
>>> This looks like exactly what we need! Any objections?
>>>
>>> --Max
>>> ___
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe@haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>>
>>
>>
>>
>>-- 
>>We can't solve problems by using the same kind of thinking we used when we
>>created them.
>>   - A. Einstein
>>___
>>Haskell-Cafe mailing list
>>Haskell-Cafe@haskell.org
>>http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How to create an online poll

[gregg reynolds]

But what about the side effects?

Rick R  wrote:

>I'm sure Premier Election Solutions (formerly Diebold) can provide us with
>an online voting solution.
>Their value-add services allows us to set the outcome beforehand, so, in
>effect, the the voting process will be determinate. Which is certainly of
>interest to Haskell coders.
>
>
>On Wed, Feb 18, 2009 at 4:05 PM, Max Rabkin  wrote:
>
>> On Wed, Feb 18, 2009 at 10:40 PM, Anton van Straaten
>>  wrote:
>> > There's also the Condorcet Internet Voting Service:
>> >
>> >  http://www.cs.cornell.edu/andru/civs.html
>>
>> This looks like exactly what we need! Any objections?
>>
>> --Max
>> ___
>> Haskell-Cafe mailing list
>> Haskell-Cafe@haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
>
>-- 
>We can't solve problems by using the same kind of thinking we used when we
>created them.
>   - A. Einstein
>___
>Haskell-Cafe mailing list
>Haskell-Cafe@haskell.org
>http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How to create an online poll

[gregg reynolds]

See also www.surveymonkey.com

Bulat Ziganshin  wrote:

>Hello haskell-cafe,
>
>http://zohopolls.com/
>
>-- 
>Best regards,
> Bulat  mailto:bulat.zigans...@gmail.com
>
>___
>Haskell-Cafe mailing list
>Haskell-Cafe@haskell.org
>http://www.haskell.org/mailman/listinfo/haskell-cafe
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Intergalactic Telefunctors

[Gregg Reynolds]

On Sun, Feb 15, 2009 at 12:45 PM, Anton van Straaten  wrote:

> Gregg Reynolds wrote:
>
>> Action-at-a-distance is a metaphor meant to enliven the concept.
>>
>
> Kind of like the container metaphor?
>

Yes, only, different.  Non-pernicious.  ;)
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Intergalactic Telefunctors

[Gregg Reynolds]

On Sun, Feb 15, 2009 at 11:53 AM, Tillmann Rendel  wrote:

> Gregg Reynolds wrote:
>
>> BTW, I'm not talking about Haskell's Functor class, I guess I should
>> have made that clear.  I'm talking about category theory, as the
>> semantic framework for thinking about Haskell.
>
>
Don't forget the part explaining this is just a sketch.

>
>>
> In that case, I even less see why you are not introducing category theory
> proper. Certainly, if one wants to use a semantic framework for thinking
> about something, one should use the real thing, not some metaphors.
>
>  The idea is that each type (category) is a distinct universe.  The
>> essential
>> point about functors cross boundaries from one category to another.
>>
>
> What are the categories you are talking about here?
>

Take your pick.

>
>
>  Moreover, you are mixing in the subject of algebraic data types (all we
>>> know about (a, b) is that (,), fst and snd exist).
>>>
>>>
>> It's straight out of category theory.  See Pierce
>> http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=7986
>>
>
> Which part specifically?
>

Sections 1.5, 1.6, 1.9, 2.1, etc.

 Personally, I do not see why one should explain something easy like
>> functors in terms of something complicated like quantum entanglement.
>>
>
> The metaphor is action-at-a-distance.  Quantum entanglement is a vivid way
> of conveying it since it is so strange, but true.  Obviously one is not
> expected to understand quantum entanglement, only the idea of two things
> linked "invisibly" across a boundary.
>

How does the fact that a morphism exists between two objects in some
> category link these objects together? It doesn't change the objects at all.
> In your own words: How can action (at-a-distance) be about mathematical
> values?
>

Not between two objects in some category; between two objects in different
categories.  That's the whole point.  Functors preserve structure.
Action-at-a-distance is a metaphor meant to enliven the concept.  You use a
map in your home category to map remote objects, by beaming it up through
the telefunctor.  Your map stays home but is quantum entangled with the
remote map.  Heh heh.  I'm not saying it's for everybody, but I think it's
kinda fun.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Intergalactic Telefunctors

[Gregg Reynolds]

On Sun, Feb 15, 2009 at 11:09 AM, Tillmann Rendel  wrote:

> Gregg Reynolds wrote:
>
>> Came up with an alternative to the container metaphor for functors that
>> you
>> might find amusing:  http://syntax.wikidot.com/blog:9
>>
>
> You seem to describe Bifunctors (two objects from one category are mapped
> to one object in another category), but Haskell's Functor class is about
> Endofunctors (one object in one category is mapped to an object in the same
> category). Therefore, your insistence on the alien


Yeah, it needs work, but close enough for a sketch.  BTW, I'm not talking
about Haskell's Functor class, I guess I should have made that clear.  I'm
talking about category theory, as the semantic framework for thinking about
Haskell.


> universe being totally different from our own is somewhat misleading, since
> in Haskell, we are specifically dealing with the case that the alien
> universe is just our own.
>

The idea is that each type (category) is a distinct universe.  The essential
point about functors cross boundaries from one category to another.

>
> Moreover, you are mixing in the subject of algebraic data types (all we
> know about (a, b) is that (,), fst and snd exist).
>

It's straight out of category theory.  See Pierce
http://mitpress.mit.edu/catalog/item/default.asp?ttype=2&tid=7986


> Personally, I do not see why one should explain something easy like
> functors in terms of something complicated like quantum entanglement.
>

The metaphor is action-at-a-distance.  Quantum entanglement is a vivid way
of conveying it since it is so strange, but true.  Obviously one is not
expected to understand quantum entanglement, only the idea of two things
linked "invisibly" across a boundary.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Intergalactic Telefunctors

[Gregg Reynolds]

Came up with an alternative to the container metaphor for functors that you
might find amusing:  http://syntax.wikidot.com/blog:9
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] IO semantics and evaluation - summary

[Gregg Reynolds]

On Sat, Feb 14, 2009 at 9:15 AM, Stuart Cook  wrote:

> From "Fixing Haskell IO":
> > We can summarize the SDIOH (Standard Definition of IO in Haskell)
> > as "a value of type IO a is a value, that performs, then delivers
> > a value of type a".
>
> I think you've already made a critical mistake here. The quotes you
> give all describe an IO value as something that "when performed"
> results in input/output, whereas your summary describes it as
> something "that performs". The original quotations suggest that some
>
outside agent interprets the values and performs the actions they
> denote, whereas it is your summary that has made the linguistic
> shift to values that dance about on tables of their own accord.
>

I see you point, and it perfectly illustrates the problem of ambiguity (
http://syntax.wikidot.com/blog:5).  "Action" and "Performance" are even more
ambiguous than "computation" and "evaluation".  The natural analog to the
SDIOH is theatrical performance.  Where is the action, on the page or on the
boards?  Who performs the action, the character or the thespian?  Whose
action is it?  Even if we settle on these questions, we have to account for
"delivers a value".  What does the performance of the action of Hamlet
deliver?  Dead Polonius?  Catharsis?

In the end it doesn't matter how one interprets "action that is performed";
either way, there must be an agent.  No agent, no performance.  As you point
out, the SDIOH can be read as positing an "outside agent"; it can also be
read to posit the value itself as performer (which must interact with an
outside agent).  All of which leads to the very interesting philosophical
question of what a program process actually //is//: an agent acting on a
computer, or a script for the computer to enact (qua agent/thespian).
Either way the SDIOH effectively tries to incorporate action/agency into the
formal semantics.

My proposition is just that we avoid the whole mess by eliminating notions
like action,  performance, and delivery.  Split the semantics into internal
(standard denotational stuff) and external (interpretation, which can also
be represented mathematically), and you get a clearer, cleaner, simpler
picture with no philosophical complications.  I'm working on some diagrams
and simpler language; once I'm done I guess I'll find out.

>
> In my mind, Haskell programs never actually "do" anything. Instead
> they merely denote a value of type IO () that consists of tokens
> representing input/output primitives, glued together by pure
> functions. It is the job of the runtime to take that value and
> actually modify the world in the manner described by the program.


I wouldn't try to talk you out of whatever works for you.  Just scratching a
rather persistent itch about clear, simple, formal, complete representations
of the intersection of math and the world.

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] IO semantics and evaluation - summary

[Gregg Reynolds]

Hi Daryoush,

2009/2/13 Daryoush Mehrtash 

> I have been trying to figure out the distinction between value, function
> and computation. You raised a few points that I am not sure about.
>
>
> In " "Computation" considered harmful. "Value" not so hot either." you
> said:
>
> I still don't like it; a lambda expression is not a computation, it's a
> formal *representation* of a mathematical object (a *value*).
>
>
> Isn't the lambda expression a representation of  something (potentially
> with recursion) that yields "a value" and not the value itself?   Even
> integer which we think of as values are represented in the same way:
> http://safalra.com/science/lambda-calculus/integer-arithmetic/
>

Excellent question, and it illustrates the problem of "abstraction
management" very nicely.  The way Church presented the lambda operator in
"Introduction to Mathematical Logic" is very instructive.  The basic idea
was how to avoid having to name functions.  This is a very pragmatic
concern; if we didn't have the lambda operator, we would have to invent a
name for every function we want to discuss, which would quickly lead to
unmanageable clutter for both writer and reader.  Church put it in terms
like this:  "x + 2" is a formula, but it doesn't denote anything, since x is
free.  It's not completely devoid of meaning - we get the "+ 2" part - but
it's an "open sentence": not a function, not a value (or: not the name of a
function or value).  But there is a function /associated/ with the formula;
we can denote that function, but only by introducing a name: f x = x + 2.
Now f denotes the function associated with the formula.  Which means we have
two things: syntax, and semantics.  Actually three things, since the name f
is a thing.  The lambda operator just allows us to do the same thing without
names:  the expression "lambda x.x+2" denotes the function associated with
the form x + 2.

So a lambda abstraction expression denotes a function without naming it.
IOW, the function is not the formula; it is an abstract mathematical thing.
A lambda application expression - e.g. (\x -> x + 2)3 denotes application of
the function to an argument.  Here '3' names a "value"; but the value and
the name are distinct.  Lambda calculus thinks of function application in
terms of rewriting forms - it's a calculus, it just manipulates the symbolic
forms.  In other words, the fact that \x -> x + 2 and 3 denote values isn't
important; we say the application denotes 5 because of syntactic rules.  5
is just a symbol that replaces the application expression.

The contrast with ZF set theory helps.  In a set theoretic account,
functions are just sets of ordered pairs.  Application just projects the
second element of the function pair whose first element is equal to the
argument.  The notion of algorithm or computation is totally absent; that's
why ZF is so attractive for semantics.  We only want to know what an
expression means, not how its meaning was discovererd.

So even though lambda calculus may used to describe the symbolic
manipulations needed to find the value of an application, it is not accurate
to say that a lambda expression represents a computation or something that
yields a value, as you put it.  Or at any rate that it /only/ represents a
computation.  It is entirely legitimate to say that "(\x -> x+2)3" denotes 5
(or more accurately, the value represented by the symbol '5'); that
represents the set theoretic perspective.  But lambda calculus licenses us
the think of the same expression as a representation of the reduction chain
leading to the symbol '5'.  So it really depends on your perspective.


>
> In " Fixing Haskell IO" you say:
>
> This "works" well enough; GHC manages to perform IO. But it doesn't fly
>> mathematically. Mathematical objects *never* act, sing, dance, or 
>> *do*anything. They just are. A value that acts is an oxymoron.
>>
>
>
> I guess I am not sure what a "mathematical object" is.   Do you consider
> Newton method a mathematical object?   What would be the "value" :
> http://en.wikipedia.org/wiki/Newton's_method#Square_root_of_a_number
>

Again, it all depends on perspective.  A formal method can be considered a
mathematical object: a sequence.  Just like a lambda expression, viewed as a
representation of a sequence of reductions.  But here again, the
representation and the thing represented are not the same.  Newton's method
is an algorithm, which exists independently of any particular
representation, just like the integer "three" is independent of the symbolic
conventions we use to denote it.   So Newton's method can be considered a
value, just as an algorithm is a kind of value, in the abstract.  And the
function "sqrt" can be considered a value, independent of any algorithm.
Application of Newton's method - note I said "application", not "syntactic
representation of application" can be thought of as a value, or an
algorithmic 

[Haskell-cafe] IO semantics and evaluation - summary

[Gregg Reynolds]

Many thanks to everybody who tried to set me straight on the thread about IO
monad and evaluation semantics.  I've begun summarizing the info, and I
believe I've come up with a much better way of explaining IO; just flip the
semantic perspective, and think in terms of interpretations instead of
actions.  Voila!  Oxymoron (values that perform actions) eliminated.   See
the "Computation considered harmful" and "Fixing Haskell IO" articles at
http://syntax.wikidot.com/blog

Naturally I would be grateful for any corrections/comments.

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] The Haskell re-branding exercise

[Gregg Reynolds]

On Sat, Feb 7, 2009 at 11:18 AM, Paul Johnson  wrote:

> Paul Johnson wrote:
>
>> A call has gone out <
>> http://www.haskell.org/pipermail/haskell-cafe/2008-December/051836.html>
>> for a new logo for Haskell.  Candidates (including a couple <
>> http://www.haskell.org/haskellwiki/Image:Haskell-logo-revolution.png> of
>> mine )
>> are accumulating here <
>> http://www.haskell.org/haskellwiki/Haskell_logos/New_logo_ideas>.  There
>> has also been a long thread on the Haskell Cafe mailing list.
>>
>>  So what's happening about this?
>

I know I'm late to the party, but here's an observation anyway.  It might be
better to settle on an emblem first, and then a logo.  Lambda is popular for
functional languages, but it's not a distinctive feature of Haskell.  What
is distinctive of Haskell is category theory in general and the monad in
particular.  Both of which are strongly reminiscent of Alchemy.  Believe it
or not, it's possible to see the operations of the monad as the exact analog
of certain aspects of Alchemy (I'm working on a detailed exposition.)

  Monad as Philosopher's Stone?  Galleries of Alchemical emblems and symbols
are easily found on the web; see for example the symbol for composition at
http://www.iridius.info/current/info/

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 10:17 PM, Richard O'Keefe  wrote:

>
> On 10 Feb 2009, at 5:07 pm, Gregg Reynolds wrote:
>
>> Thanks.  I see the error of my ways.  So, IO expressions must be evaluated
>> if they are in the chain leading to main.
>>
>
>
> We need some standard terminology to distinguish
> between *evaluating* an expression and *performing*
> the result of an expression of type IO something.
>

Indeed.  Wrote a blog article about this proposing a semiotic approach:
http://syntax.wikidot.com/blog:4

>
> An IO expression that is passed to a function at a
> strict position must be evaluated whether the result
> is performed or not.
>
> An IO expression whose result will be performed must
> be evaluated before that performance can take place.
>

Is the result of evaluation a thunk/suspension/closer?


>
> (Dash it, this really is getting us into White Knight land.)
>

What's White Knight land?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Haskell Fest

[Gregg Reynolds]

Just be careful.  The judge uses lazy evaluation, so if you get arrested you
might spend 20 years in the holding pen.  On the bright side, you can pay
for stuff whenever you feel like it.

2009/2/9 Lyle Kopnicky 

> Looks like a lot of fun!
>
> http://www.haskellchamber.com/page6.html
>
> ___
> Haskell-Cafe mailing list
> Haskell-Cafe@haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 8:37 PM, Richard O'Keefe  wrote:

>
> There isn't any "application f e".
> Any human reader who does that is simply WRONG to do so.
>

Sorry, should have written f*

>
> In your fragmentary example,  may be discarded
> EVEN IF it contains IO expressions, it's only if they are linked into
> the IO chain using >> and/or >>= that the environment will perform
> their values.
>

Thanks.  I see the error of my ways.  So, IO expressions must be evaluated
if they are in the chain leading to main.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 11:06 AM, Tillmann Rendel  wrote:

> Gregg Reynolds wrote::
>
>> My original question was motivated by the observation that a human reader
>> of
>> an expression of the form "e >>= f" , on seeing that f is constant, may
>> pull
>> the constant value out of f, disregard e and dispense with the application
>> f
>> e.
>>
>
> While a human reader may well do that, but it would be correct or wrong
> depending on the definition of >>=. The same is of course true for
> compilers. By the way, there is no "application f e".
>

I guess it would help if I got the notation right.  My intended meaning was
f* e, where * is the Kleisli star.  Sorry about that.

>
>
> An example where it would be wrong to ignore e:
>
>  sum ([1, 2] >>= const [21])
>
> This expression should evaluate to sum [21, 21] = 42, not sum [21] = 21.
>

Sigh.  I hate it when this happens.  Just when I thought I had it figured
out, it turns out I'm clueless.  This is very enlightening and should
definitely be included in any monad tutorial.  Actually you don't even need
"sum" and "const" to demo the point,  "[1,2] >>= \x -> [21]" evals to "[21,
21]" in ghci.  And I have absolutely no idea why.  Very mysterious, the
Kleisli star.  :(

Back to the drawing board!

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Formal semantics for Haskell?

[gregg reynolds]

Is that () or _|_? ;)

Tim Newsham  wrote:

>null___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Formal semantics for Haskell?

[Gregg Reynolds]

ML has a formal definition[1]; why not Haskell?  Would this be a Good Thing,
or a Waste Of Time?  The Report strikes me as a hybrid of formal and
informal.  I guess that's not a problem so far, but there aren't that many
implementations; if we had dozens, how could we verify conformance?  A
formal semantics would be useful, but it would also be Fun to use Category
Theory notation in a language definition.

Such a task would be way beyond my abilities, but I have come up with an
idea for a formal semantics of IO and other non-deterministic elements of
the language that I think is kind of interesting.  It's inspired by Category
Theory and the Z specification language.   See  my (brief) blog
article
.

Actually, I'm in a state of rather intense euphoria about it, so a bucket of
cold water realism over my head might be a Good Thing.  Then I could get
some sleep instead of obsessing about category theory and Haskell.  :)

I propose any formal definition include the following warning, modeled on
Knuth's warning about MetaFont:

  WARNING:  Haskell can be hazardous to your other interests.  Once you get
hooked, you will develop intense feelings about language design; semantic
models will intrude on the program texts you read.  And you will perpetually
be thinking of improvements to the programs that you see everywhere,
including those of your own design.

Thanks,

gregg


[1] The Definition of Standard ML (Revised); a preview is on Google Books
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 7:17 AM, Lennart Augustsson
wrote:

> Just to clarify a little.
> If you implement the IO monad in a sane way (as some kind of state
> monad or continuation monad) then the compiler can optimize e>>=f even
> for the IO monad.  The implementation of >>= will ensure the
> sequencing of effects in e before effects in f.


I think this answers one of my questions about the relation of category
theory to Haskell. Bind is an implementation of the Kleisli star, but the
latter, being abstract, may encode data dependency but not sequence.  The IO
implementation of >>= must ensure sequence, regardless of data dependency
(e.g. even for putChar 'a' >>= \x -> putChar 'c').

So if we wanted to write a Haskell specification with more formality and
detail than the Report, we could say that the IO monad must implement the
Kleisli star operator, but that would not be enough, we would also have to
require that the implementation ensure sequencing.  IOW, Kleisli star
implementation plus a constraint on the implementation.  Does that sound
right?

>
> The IO monad is less magic than you seem to think it is. :)
>

Any sufficiently advanced technology is isomorphic to magic.  ;)

(http://www.quotationspage.com/quote/776.html)

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Monad explanation

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 5:32 AM, Sittampalam, Ganesh <
ganesh.sittampa...@credit-suisse.com> wrote:

>
> > My bad, I restate:  a value cannot be both static and dynamic.  Or an
> > object and a morphism.  Or an element and a function.  Sure, you can
> > treat a morphism as an object, but only by moving to a higher (or
> > different) level of abstraction.  That doesn't erase the difference
> > between object and morphism.  If you do erase that difference you end
> > up with mush.  getChar /looks/ like an object, but semantically it
> > must be a morphism.  But it can't be a function, since it is
> > non-deterministic.   So actually the logical contradiction comes from
> > the nature of the beast.
> >
> > Another reason it's confusing to newcomers:  it's typed as "IO Char",
> > which looks like a type constructor.  One would expect getChar to
> > yield a value of type IO Char, no?  But it delivers a Char instead.
> > This is way confusing.  So I take "type IO foo" to mean "type foo,
> > after a side effect".  In a sense "getChar :: IO Char" isn't even a
> > true type signature.
>
> It does yield a value of type IO Char, which it also happens that you
> can ask the Haskell runtime to interpret by combining it with other
> IO values using >>= and invoking it from the top-level.
> *When interpreted in this way* it delivers a Char, but that's precisely
> the point at which we move to the different level of abstraction you
> mention above.


Right; "implementation of IO" means also an implementation for >>=, not just
the IO operators.  I hadn't thought about that but it's hugely important for
the exposition of monads and IO.

"The IO Char indicates that getChar, when invoked, performs some action
which returns a character." (Gentle Intro, typical of many expositions.)

That, plus the form of \x -> putChar x used with >>=, plus the fact that one
can do getChar at the ghci command line, plus all the other stuff - it all
adds up to exasperation.

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Sun, Feb 8, 2009 at 6:25 PM, Richard O'Keefe  wrote:

>
> On 6 Feb 2009, at 4:20 am, Gregg Reynolds wrote:
>
>>  However, consider:
>>
>>getChar >>= \x -> getChar
>>
>> An optimizer can see that the result of the first getChar is discarded and
>> replace the entire expression with one getChar without changing the formal
>> semantics.
>>
>
> But the result of the first getChar is *NOT* discarded.
> **As an analogy**, think of the type IO t as (World -> (t,World))
> for some hidden type World, and
>getChar w = (c, w')
>-- get a character c out of world w somehow,
>-- changing w to w' as you go
>(f >>= g) w = let (v,w') = f w in (g v) w'
>
> In this analogy, you see that the result of getChar is a value of
> type IO Char (not of type Char), and that while the character
> part of the result of performing the result of getChar may be
> discarded, the "changed world" part is NOT.


That's an implementation detail.  It doesn't account for other possible IO
implementations.

My original question was motivated by the observation that a human reader of
an expression of the form "e >>= f" , on seeing that f is constant, may pull
the constant value out of f, disregard e and dispense with the application f
e.  So can a compiler, unless IO expressions are involved, in which case
such optimizations are forbidden.  I wondered if that was due to the
semantics of >>= or the semantics of IO.

To summarize what I've concluded thanks to the helpful people on
haskell-cafe:

The compiler can optimize e >>= f except for any IO expressions in e and f.
IO expressions must be evaluated, due to the semantics of IO.  The may not
be disregarded, memoized, or substituted.  IO semantics may be implemented
in different ways by different compilers; these implementation techniques
are not part of the formal semantics of the language, which may be expressed
as above:  IO expressions must be evaluated wherever and whenever they
occur.

The bind operator >>= enforces sequencing on arguments containing IO
expressions, but does not force evaluation.  Even bind expressions involving
IO may be optimized.  For example:

  getChar >>= \x -> .. putChar 'c'

The compiler may discard  (assuming it contains no IO
expressions), but it must evaluate getChar and putChar (due to IO semantics)
in the correct order (due to bind semantics).

Thanks all,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Monad explanation

[Gregg Reynolds]

On Mon, Feb 9, 2009 at 4:38 AM, Tony Morris  wrote:

> -BEGIN PGP SIGNED MESSAGE-
> Hash: SHA1
>
> I also agree it is a value.
> The original post was attempting to make a distinction that does not
> exist. I deliberately avoided that topic.
>
> "A thing cannot be both a value and a function, but e,g, getChar"
>
> My original intent was to hope the poster reconsidered the whole post.
> You've blown my cover :)
>

My bad, I restate:  a value cannot be both static and dynamic.  Or an object
and a morphism.  Or an element and a function.  Sure, you can treat a
morphism as an object, but only by moving to a higher (or different) level
of abstraction.  That doesn't erase the difference between object and
morphism.  If you do erase that difference you end up with mush.  getChar
/looks/ like an object, but semantically it must be a morphism.  But it
can't be a function, since it is non-deterministic.   So actually the
logical contradiction comes from the nature of the beast.

Another reason it's confusing to newcomers:  it's typed as "IO Char", which
looks like a type constructor.  One would expect getChar to yield a value of
type IO Char, no?  But it delivers a Char instead.  This is way confusing.
So I take "type IO foo" to mean "type foo, after a side effect".  In a sense
"getChar :: IO Char" isn't even a true type signature.

In any case, many thanks to all who have contributed to the thread.  It's
sharpened my thinking revealed weaknesses in my terminology, and I expect
I'll make my inevitable contribution to the infinite Haskell tutorial on the
topic before too long.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Monad explanation

[Gregg Reynolds]

On Sun, Feb 8, 2009 at 6:39 PM, Richard O'Keefe  wrote:

>
> is a good one.  If you want to say that "a mathematical value with
> a non-mathematical effect" is nonsensical, more power to you.  I said
> I don't want to get far into White Knight territory.  As long as you
> can agree "A mathematical value INTERPRETED BY a physical engine can
> have physical effects", we're home and dry.
>

Here's an analogy that will make the logical contradiction clear.  Forget
computers and assume you have been asked to referee a paper containing a
proof with the following passage:

   Let x = ___ (Please fill in the blank)

I think you will agree that would be plainly nonsensical.  It's logically
equivalent to an input operation ("getInt").

Now back to computers.  Given a program text containing the symbol '3', the
computer will provide a physical representation: an electromagnetic pattern
in a bit of silicon.  That's a value; the pattern is to be interpreted as a
datum; it is not to be executed.  For "getChar", the computer will also
provide such a pattern, but this pattern is to be interpreted as executable
code, not as a datum.  Now suppose we also have an ordinary function like
"Add2"; it too will be represented as an electromagnetic pattern, to be
interpreted as executable code.  getChar and Add2 are not data, except in
the trivial sense that all code is data.  All three "have an effect" only in
the trivial sense that they are physically represented.

In all three cases, the symbolic representation is isomorphic to the
physical representation.  The 3 will not be executed.  When Add2 is
executed, the ensuing process is isomorphic to the mathematical function so
defined.  But when getChar is executed, the ensuing process is not
isomorphic to a mathematical function.  The process interacts with the
non-mathematical world, which a mathematical function can never do.  So it
has a side effect along with its ordinary representational effect.

The point being that the metalanguage commonly used to describe IO in
Haskell contains a logical contradiction.  A thing cannot be both a value
and a function, but e,g, getChar behaves like a function and has the type
signature of a value.  I believe this is part of the reason the IO monad is
troublesome for beginners (I speak from experience).

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Moggi :: CT -> Hask

[Gregg Reynolds]

Hi Dan,

On Sat, Feb 7, 2009 at 12:00 PM, Dan Doel  wrote:

> On Saturday 07 February 2009 12:11:29 pm Gregg Reynolds wrote:
>
> As far as I know, Moggi didn't really have anything directly to do with
> Haskell. He pioneered the idea of monads being useful in denotational
> semantics. But it was Wadler that recognized that they'd be useful for
> actually writing functional programs (see his "The Essence of Functional
> Programming"). So one might say that it was his doing that brought monads
> to
> Haskell proper.
>

>From what I've read Wadler was clearly the guy who thought of using monads
in Haskell, but he explicitly credits Moggi for coming up with the general
idea.  Moggi just as clearly knew he was on to something powerful and useful
(e.g. something " that could lead to the introduction of higher order
modules in programming languages like ADA or ML").  What I would be
interested in knowing is whether it was Wadler or Moggi who first realized
monads (and CT) could be encoded directly in a target language, not just in
a semantic metalanguage.  Plus there were other people working in the same
area; I just don't know the detailed history.  Might be a good subject for a
blog post for somebody who does.

FYI I made a few corrections to my original post.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Semantic web

[gregg reynolds]

Anybody implementing rdf or owl  stuff in haskell?  Seems like a natural fit.

G___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: Moggi :: CT -> Hask

[Gregg Reynolds]

Correction: the correct response is:  "Nothing."

On Sat, Feb 7, 2009 at 11:11 AM, Gregg Reynolds  wrote:
> Hi,
>
> I had a monadic revelation at about 3 am.  The answer to the question
> "what is an IO value, really?" is "who cares?"  I just posted a blog
> entry discussing how CT found it's way from Moggi into Haskell at
> http://syntax.wikidot.com/blog (hence the title; Moggi as functor).
> It addresses the question of what such things are and why Moggi's
> insight is so brilliant.  Feedback welcome, but please remember this
> is coming from a non-mathematician who likes to write.  If you find
> anything there that outrages your inner Russell, please correct me,
> but be gentle.
>
> Thanks,
>
> gregg
>
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Moggi :: CT -> Hask

[Gregg Reynolds]

Hi,

I had a monadic revelation at about 3 am.  The answer to the question
"what is an IO value, really?" is "who cares?"  I just posted a blog
entry discussing how CT found it's way from Moggi into Haskell at
http://syntax.wikidot.com/blog (hence the title; Moggi as functor).
It addresses the question of what such things are and why Moggi's
insight is so brilliant.  Feedback welcome, but please remember this
is coming from a non-mathematician who likes to write.  If you find
anything there that outrages your inner Russell, please correct me,
but be gentle.

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] morphisms in IO

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 10:32 PM, Dan Weston  wrote:
> I truly have no idea what you are saying (and probably not even what I am
> saying), but I suspect:
>
> a) You are calling IO the target category of applying the functor IO [taking
> a to IO a and (a->b) to (IO a -> IO b)] to Hask.
>
> b) This category is hardly bereft, nor discrete. Its morphisms are IO a ->
> IO b.

Well, that's a function in Haskell, yes; but does it represent a
morphism /in/ the category?  It looks more like a Functor morphism to
me.
>
> c) What you are calling a "bereft" category is an empty category. Without
> (identity) morphisms, there can be no objects. There is only one such

Right, I meant other than Id morphisms.  I guess "discrete" is the correct term.

> category (the empty category), so naturally any two such are isomorphic (for
> what it's worth, which I suspect is not much).

Thanks,

g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] morphisms in IO

[Gregg Reynolds]

I'm working on a radically different way of looking at IO.  Before I
post it and make a fool of myself, I'd appreciate a reality check on
the following points:

a)  Can IO be thought of as a category?  I think the answer is yes.

b)  If it is a category, what are its morphisms?  I think the answer
is: it has no morphisms.  The morphisms available are natural
transformations or functors, and thus not /in/ the category.
Alternatively: we have no means of directly naming its values, so the
only way we can operate on its values is to use morphisms from the
outside (operating on construction expressions qua morphisms.)

c)  All categories with no morphisms ("bereft categories"?) are
isomorphic (to each other).  I think yes.

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 7:19 PM, wren ng thornton  wrote:
> Gregg Reynolds wrote:

>> as the formal semantics of the language are concerned, there's no
>> essential difference between  "getChar >>= \x -> getChar" and " Foo 3
>>>>
>>>> = \x -> Foo 7 " for some data constructor Foo.  I should think the
>>
>> latter would be optimized; if so, why not the former?  The presence of
>> some hidden (from me, anyway) semantics is inescapable.
>
> There's no reason to assume the latter would be "optimized" either.
> Consider:
>
>> data NotIO a = NotIO String a
>>
>> instance Monad NotIO where
>> return x  = NotIO "" x
>> (NotIO s x) >>= f = (\(NotIO z y) -> NotIO (s++z) y) (f x)
>>
>> notGetChar = NotIO "foo" 'a'
>
> Let's consider your example:
>
>notGetChar >>= \x -> notGetChar
>  ==
>(NotIO "foo" 'a') >>= (\x -> NotIO "foo" 'a')
>  ==
>(\(NotIO z y) -> NotIO ("foo"++z) y) ((\x -> NotIO "foo" 'a') 'a')
>  ==
>(\(NotIO z y) -> NotIO ("foo"++z) y) (NotIO "foo" 'a')
>  ==
>NotIO ("foo"++"foo") 'a'
>

You've defined >>= in such a way that it carries additional semantic
weight.  My example doesn't do that.  Bind can be thought of as an
"augmented application" operator: x >>= f applies f to x, but it may
fiddle with x first.  If it doesn't then it amounts to ordinary
function application, which can be optimized out.  That's the point of
my example: data constructors don't munge their arguments, and getChar
is essentially a data constructor.

> NotIO has a Chars for "side effects". IO is a perfectly fine mathematical
> object, the only difference is that it is appending sequences of an abstract

Gotcha!  "appending sequences" is not something mathematical values
are inclined to do.  They neither spin nor toil, let alone append.
The dominant idiom - "IO values are actions" just doesn't work if you
want formal semantics, no matter how useful it may be pedagogically.
>
> The only way we can optimize away one of the calls to notGetChar (or any
> other monadic function) is if we can guarantee that no other computation
> will use either the monoidal values or the "contained" values associated
> with it. IO is defined with a bind operator that's strict in the monoidal
> value, which means we can never remove things (unless, perhaps, we can

Ok; but where does it say that in the language definition?  I
understand how it all works, but that comes from the many informal
narrative expositions; my point is that if you tried to write a formal
semantics for Haskell, a la ML, you couldn't do it without coming up
with a different story for IO.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Monad explanation

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 1:46 PM, Lennart Augustsson
 wrote:
> You are absolutely right.  The statement
>  "The values of the IO monad are programs that do IO. "
> is somewhat nonsensical. Values don't do anything, they just are.

Whew!  So I'm not crazy.  I was starting to wonder.

> But values of the IO monad *describe* how to do IO; they can be seen
> as a recipe for doing IO.
> A recipe doesn't cook a dish, but when the recipe is executed by a
> cook they creates a dish.
> An IO values doesn't do IO, but when it is executed by the runtime
> system IO happens.
>
> This is one way of interpreting what the IO type means.
> (Another one is to say that Haskell is just an imperative programming
> language, but any imperative actions show up in the type.)
>

Thanks very much to you and everybody who contributed on the thread.
It's amazing how much one can learn on this list.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 11:22 AM, Gleb Alexeyev  wrote:
> Gregg Reynolds wrote:
>
>> Are you saying that using equations to add a level of indirection
>> prevents optimization?  I still don't see it - discarding x doesn't
>> change the semantics, so a good compiler /should/ do this.  How is
>> this different from optimizing out application of a constant function?
>>
>
> Perhaps my example doesn't work, so I'll try another example.
> As you know, (>>=) is just an (overloaded) higher-order function.
> Let's consider another higher-order function, map. The expression
>> map (\x -> 42) [1..3]
> evaluates to [42, 42, 42].
> As you can see, the function (\x -> 42) passed to map ignores its first
> argument. Would you expect the compiler to discard the call to map?

No, but I might expect it to discard the function application and just
replace each element of the list with 42.  Which it may do at compile
time.  Plus, it will only be evaluated once, no matter how many times
the expression occurs, since lazy evaluation memoizes results.
>
> Can you see the analogy? The shapes of the two expressions, map (\x -> 42)
> [1..3] and (>>=) getChar (\x -> getChar) are similar.
>
> (>>=) is a combinator just like map, you cannot optimize it away in general.

Ok, I see what you're getting at, but I have to think about it some more.

Here's a restatement that might make my puzzlement more clear.  Suppose we have

   f = \x -> 42

Then I would expect the compiler to replace each expression of the
form f x with 42, for all x.

Now suppose we write  7 >>= \x -> 42.  It seems to me that a compiler
could examine that expression, conclude that it is constant, and
replace it with the expression 42.  So far as I know, there's nothing
in the semantics of Haskell to forbid this, so why not do it?  There
are no side effects, and an optimizer can always substitute equals for
equals, no?  (Let's disregard the fact that such optimizations may be
hard or expensive.)

This is different from map, because unlike map it doesn't need to
perform a computation (i.e. execute the function) to arrive at the
final value; it only has to analyze the function (which is computation
but not computation of the function itself.)

Now getChar is a value of type IO Char, by definition.  That means
mathematical value - "an action that does some IO" won't cut it in a
formal semantics, since there is no way to express "does some IO"
formally.  Values is values; they don't "do" anything.  So we should
be able to replace 7 and 42 above by getChar, and do the same
optimization.

Do you see why this is problematic for me?  In any case, you're
responses (and the others) have been quite useful and have helped me
work through some problems with a rather radical idea I have to
address this that I hope to write up this weekend.

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 11:12 AM, Andrew Wagner  wrote:
>
>
>> Are you saying that using equations to add a level of indirection
>> prevents optimization?  I still don't see it - discarding x doesn't
>> change the semantics, so a good compiler /should/ do this.  How is
>> this different from optimizing out application of a constant function?
>
> No, no compiler should change "getChar >>= \x -> getChar" to just getChar,
> because it's just wrong. The first will try to read in two values of type
> Char, the second will only try to read one. Side effects aren't THAT hated!

Right, but that's only because the compiler either somehow knows about
side effects or there is some other mechanism - e.g. an implicit World
token that gets passed around - that prevents optiimization.  As far
as the formal semantics of the language are concerned, there's no
essential difference between  "getChar >>= \x -> getChar" and " Foo 3
>>= \x -> Foo 7 " for some data constructor Foo.  I should think the
latter would be optimized; if so, why not the former?  The presence of
some hidden (from me, anyway) semantics is inescapable.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 10:49 AM, Gleb Alexeyev  wrote:
> Gregg Reynolds wrote:
>  > I must be misunderstanding something.  I don't know if it would be
>>
>> optimized out, but I see no reason why it couldn't be.  There's no data
>> dependency, right?
>
> Of course there is data dependency. In my example, where IO is defined as a
> (generalized) algebraic datatype, the value of getChar is GetChar.
> The value of 'getChar >>= \x -> getChar' is 'Bind GetChar (\x -> GetChar'.
> 'x' is not used anywhere, but this doesn't change the fact that these are
> totally different values, no sane compiler would prove them equal.

Are you saying that using equations to add a level of indirection
prevents optimization?  I still don't see it - discarding x doesn't
change the semantics, so a good compiler /should/ do this.  How is
this different from optimizing out application of a constant function?

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 10:26 AM,   wrote:
>
> x >>= f does not mean "apply f to x", it means "do x, and then do f with
> the result of x". Bind is a sequencing operator rather than an
> application operator.

Sequencing is a side effect of data dependency.  What I should have
said is x >>= f means "evaluate x and f (in any order), /then/ apply f
to x".  In a non-IO monad, x can be discarded if f does not depend on
it.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 10:00 AM, Lennart Augustsson
 wrote:
>
> There's nothing magic about IO when it comes to monad semantics.
> If you take ghc's implementation of IO, it's a state monad.

Doesn't that mean the semantics are defined by the implementation?  My
problem is that I'm not seeing how correct eval sequencing can be
forced unless a magic token is passed around, which means that /some/
such hidden semantics must be part of the formal semantics of IO.  In
other words, it's not enough for it to be a monad, since >>= by itself
cannot guarantee data dependency.  If it doesn't pass around the World
token, we don't get sequencing.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Re: evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 9:53 AM, Gleb Alexeyev wrote:

> Let's imagine that IO datatype is defined thus:
>
> >{-# LANGUAGE GADTs #-}
> >{-# LANGUAGE NoImplicitPrelude #-}
>
> >import Prelude(Monad, Char)
> >data IO a where
> >GetChar :: IO Char
> >Bind :: IO a -> (a -> IO b) -> IO b
>
> >getChar = GetChar
> >(>>=) = Bind
>
> It is perfectly possible to construct IO actions as values of this data
> type and execute them by some function evalIO :: IO -> Prelude.IO with the
> obvious definition. Now the question arises: do you think
> getChar >>= \x -> getChar would be optimized to getChar by compiler?
>

I must be misunderstanding something.  I don't know if it would be optimized
out, but I see no reason why it couldn't be.  There's no data dependency,
right?

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Monad explanation

[Gregg Reynolds]

On Wed, Feb 4, 2009 at 8:18 PM, Richard O'Keefe  wrote:

>
> On 5 Feb 2009, at 10:20 am, Gregg Reynolds wrote:
>
>> That's a fairly common representation, seems to work for lots of people,
>> but it caused me no end of trouble.  Values are mathematical objects; how, I
>> asked myself, can they possibly /be/ programs that do IO (or actions, or
>> computations, or )?  It doesn't make sense, says I,
>>
>
> without reference to the rest of your message, of course values can /be/
> programs.


Not "programs", but "programs that do IO".  The point of the idiom is that
there's an external side effect involved.  What sticks in my craw is that "a
mathematical value with a non-mathematical side effect" is, well,
non-mathematical and possibly nonsensical.  I know it works for some (most?)
people, but for me it lacks Geometry and Theology.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

On Thu, Feb 5, 2009 at 9:27 AM, Bulat Ziganshin
wrote:

> Hello Gregg,
>
> Thursday, February 5, 2009, 6:20:06 PM, you wrote:
>
> > An optimizer can see that the result of the first getChar is
> > discarded and replace the entire expression with one getChar without
> > changing the formal semantics.
>
> this is prohibited by using pseudo-value of type RealWorld which is
> passed through entire action stream. actually, order of execution is
> controlled by dependencies on this values
>
> http://haskell.org/haskellwiki/IO_inside
>
> Thanks.  I actually read that a few weeks ago and forgot all about it.  So
the gist is that type IO has special magic semantics.  Formal, but hidden.
Which means monad semantics are built in to the language, at least for that
type.  The Haskell Report doesn't seem to say anything about this, which
seems odd.

But then for non-IO monads, the optimization would be allowed, no?  Of
course; only the IO monad has external world behavior.

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] evaluation semantics of bind

[Gregg Reynolds]

I think I've just about got monads figured out, but there's one detail that
still escapes me.  As I understand it, a monad is a kind of programming
trick the uses data dependency to force evaluation order.  x >>= f means
apply f to x; since the value of f x depends on the value of x, the
evaluator must evaluate x before f x. However, consider:

getChar >>= \x -> getChar

An optimizer can see that the result of the first getChar is discarded and
replace the entire expression with one getChar without changing the formal
semantics.  But that would change the behavior, so to get the desired
behavior, there must be some principle that prevents this from happening,
ensuring that x >>= f always evaluates f x.

I can see that the monad laws ensure this But I haven't found anything that
states this.  Am I missing something?

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Monad explanation

[Gregg Reynolds]

On Wed, Feb 4, 2009 at 11:41 AM, Tim Newsham  wrote:

> I put up a small Monad explanation (I wouldn't quite call it
> a tutorial):
>  
> http://www.thenewsh.com/~newsham/haskell/monad.html
>

"The values of the IO monad are programs that do IO. "

That's a fairly common representation, seems to work for lots of people, but
it caused me no end of trouble.  Values are mathematical objects; how, I
asked myself, can they possibly /be/ programs that do IO (or actions, or
computations, or )?  It doesn't make sense, says I, so I
must be misunderstanding something about "values"; better spend hours and
hours researching and trying to figure this out.  But it turns out the
answer is simple: they can't.  They're not actions, or IO procedures, or
anything else other than plain old mathematical values, no different than
'2' or Int -> Char.  They happen to correspond in some way to the external
physical behavior of the program, but that correspondence is an
implementation detail beyond the scope of the formal (mathematical)
semantics of the language.  You don't even need monads for this part; they
only enter the picture in order to provide ordered evaluation.  In fact
there really aren't any "monadic values", since a monad is pure morphism;
the values at issue are "functoric values" if anything.  It's (the
implementation of) getChar the does the IO, not IO Char.

So you could say that the monad itself is a purely mathematical structure
that has the felicitous if accidental side effect of imposing temporal
sequence on the physical interpretation (events) associated with  the
program.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type and data constructors in CT

[Gregg Reynolds]

On Mon, Feb 2, 2009 at 3:27 PM, David Menendez  wrote:


> Does that help at all?
>

I think it does.  But ... it gives me crazy ideas.  Like:  a functor is a
kind of magic non-computing function!  That's why they didn't call it a
function?  We know it maps A to FA, but we don't know how (maybe we don't
care): there's no algorithm, just a functorific magic carpet that transports
us across the border to FA.  We couldn't compute FA even if we wanted to -
different categories are like alternate universes, it would be like
producing a widget in an alternate physical universe, we have no way of even
thinking of how to do that.

Ditto for data constructors as natural transformations: they don't compute,
they just do magic.  They're the CT surgeon's devious way of working on the
guts of a categorical object without getting his hands dirty with mundane
functions - getting from value A to (an?) image value of A under the functor
F, which we cannot do directly by algorithm or computation.  We do not - can
not - have an actual function that computes A's image.  We have to work
indirectly, using non-computing magic carpets - first Id takes us to Id A,
then we follow the nat trans to FA.

Ok, that probably triggers the gag reflex for a real mathematician, but it
sure sounds like a good story to me (remember, I'm taking notes for a
guide/tutorial for newbies that may or may not ever get written.)

Thanks very much for the help,

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

On Mon, Feb 2, 2009 at 2:25 PM, Ketil Malde  wrote:

> Gregg Reynolds  writes:
>
> > Just shorthand for something like "data Tcon a = Dcon a", applied to Int.
> > Any data constructor expression using an Int will yield a value of type
> Tcon
> > Int.
>
> Right.  But then the set of values is isomorphic to the set of Ints,
> right?
>

The values constructed by that particular constructor, yes; good point.
Isomorphic, but not the same.  (And also, if we have a second constructor,
what's our cardinality?  The first one "uses up" all the integers, no?
Since we can define "aleph" constructors, each of which can yield "aleph"
values, well that's a lot of values.)


>
> >> I don't follow this argument.  Are you saying you can remove a
> >> data constructor from a type, and still have the same type?  And
> >> because of this, the values of the type do not constitute a set?
>
> > Yep.
>
> I don't see why you would consider it the same type.  Since, given any
> two data types, I could remove all the data constructors, this would
> make them, and by extension, all types the same, wouldn't it?
>

I don't think so; considered as sets, they have different intensions, and
considered as predicates, they're clearly distinct even if there are no
objects.  Different names (descriptions), different things, unless we
declare they are equal.

You would probably find "When is one thing equal to another thing", by Barry
Mazur (at 
http://www.math.harvard.edu/~mazur/<http://www.math.harvard.edu/%7Emazur/>).
A fascinating discussion of equality in the context of category theory.  See
also "On Sense and Intension" at http://consc.net/papers.html

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

[Haskell-cafe] Re: type metaphysics

[Gregg Reynolds]

On Mon, Feb 2, 2009 at 11:14 PM,  wrote:

>
> I believe the original notion of type by Russell is most insightful,
> bridging the semantic notion of type (type as a set of values) and the
> syntactic notion (type system as a syntactic discipline, a statically
> decidable restriction on terms).
>
> That point is discussed at some length in Sec 3 (pp. 7-8) of
>http://okmij.org/ftp/Computation/FLOLAC/lecture.pdf
>
>
Fantastic!  That's exactly the sort (heh) of thing I was looking for.


> Incidentally, Russell has published his paper that introduced types as
> we in Computer Science know them in 1908. Last year there was 100th
> anniversary of types. I have been trying to prompt people to have a
> party and celebrate the occasion -- alas, to no avail.
>

Also the 100th anniversary of Zermelo's "Untersuchungen über die Grundlagen
der Mengenlehre I" (Investigations in the foundations of set theory) -
pretty tough competition.  Maybe a "Set Theory v. Type Theory All-star
Smackdown" would draw a crowd.  Lots of beer, mud-wrestling, monster trucks,
that sort of thing.

Thanks much,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

On Mon, Feb 2, 2009 at 12:39 PM, Ketil Malde  wrote:

> Gregg Reynolds  writes:
>
> > This gives a very interesting way of looking at Haskell type
> > constructors: a value of (say) Tcon Int is anything that satisfies
> > "isA Tcon Int".
>
> Reminiscent of arguments between dynamic and static typing camps - as
> far as I understand, a "dynamic type" is just a predicate.  So
> division by zero is a "type error", since the domain of division is
> the type of all numbers except zero.
>
> In contrast, I've always thought of (static) types as disjoint sets of
> values.
>
> > My reasoning is that we can
> > define an infinite number of data constructors for it, including at
> > least all possible polynomials (by which I mean data constructors of
> > any arity taking args of any type).
>
> I guess I don't quite understand what you mean by "Tcon Int" above.
> Could you give a concrete example of such a type?
>

Just shorthand for something like "data Tcon a = Dcon a", applied to Int.
Any data constructor expression using an Int will yield a value of type Tcon
Int.

>
> > To my naive mind this sounds suspiciously like the set of all sets,
> > so it's too big to be a set.
>
> I suspect that since types and values are separate domains, you avoid
> the complications caused by self reference.
>
> > In any case, Tcon Int does not depend on any particular constructor,
> > just as homo sapiens does not depend on any particular man.   So it
> > can't be a set because it doesn't have its members essentially.
>
> I don't follow this argument.  Are you saying you can remove a
> data constructor from a type, and still have the same type?  And
> because of this, the values of the type do not constitute a set?
>

Yep.  Well, that is /if/ you start from the "Open-World Assumption" - see
http://en.wikipedia.org/wiki/Open_World_Assumption (very important in
ontologies e.g. OWL and Description Logics).  Just because we know that e.g.
expressions like Dcon 3 yield values of type Tcon Int does not mean that we
know that those are the only such expressions.  So we can't really say
anything about how big it can be.   Who knows, it might actually be a useful
distinction for an OWL reasoner in Haskell.

>
> I guess it boils down to how "Tcon Int" does not depend on any
> particular constructor.
>

That seems like a good way of putting it.

-g
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

On Mon, Feb 2, 2009 at 11:51 AM, Lennart Augustsson
wrote:

> If we're talking Haskell types here I think it's reasonable to talk
> about the values of a type as those that we can actually express in
> the Haskell program, any other values are really besides the point.
> Well, if you have a more philosophical view of types then I guess
> there is a point, but I thought you wanted to know about Haskell
> types?
>

The metaphysics thereof.  ;)  I want to situate them in the larger
intellectual context to get a more precise answer to "what is a type,
really?"

>
> There's nothing mysterious about _|_ being a member of a set.  Say
> that you have a function (Int->Bool).  What are the possible results
> when you run this function?  You can get False, you can get True, and
> the function can fail to terminate (I'll include any kind of runtime
> error in this).
> So now we want to turn this bit of computing into mathematics, so we
> say that the result must belong to the set {False,True,_|_} where
> we've picked the name _|_ for the computation that doesn't terminate.
> Note that is is mathematics, there's no notion of non-termination
> here.  The function simply maps to one of three values.
>

I like that, thanks.

-gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] type metaphysics

[Gregg Reynolds]

Hi and thanks for the response,

On Mon, Feb 2, 2009 at 10:32 AM, Lennart Augustsson
wrote:

> Thinking of types as sets is not a bad approximation.  You need to add
> _|_ to your set of values, though.
>
> So, Bool={_|_, False, True}, Nat={_|_,Zero,Succ _|_, Succ Zero, ...}
>

I'm afraid I haven't yet wrapped my head around _|_ qua member of a set.  In
any case, I take it that sets being a reasonable /approximation/ of types
means there is a difference.

Back to metaphysics:  you pointed out that the function space is countable,
and Christopher noted that there are countably many strings that could be
used to represent a function.  So that answers my question about the size of
e.g. Tcon Int.  But then again, that's only if we're working under the
assumption that the "members" of Tcon Int are those we can express with data
constructors and no others.  If we drop that assumption,then it seems we
can't say much of anything about its size.

FWIW, what started me on this is the observation that we don't really know
anything about constructed types and values except that they are
constructed. I.e. we know that "Foo 3" is the image of 3 under Foo, and
that's all we know.  Any thing else (like operations) we must construct out
of stuff we do know (like Ints or Strings.)  This might seem trivial, but to
me it seems pretty fundamental, since it leads to the realization that we
can use one thing (e.g. Ints) to talk about something we know nothing about,
which seems to be what category theory is about.  (Amateur speaking here.)

Thanks,

gregg
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe