Re: [Haskell-cafe] Reddy on Referential Transparency
Except in the complexity gymnastics and the fragility of the conclusions. Humans can't do large scale complex brain gymnastics - that's why abstraction exists - if your proof process doesn't abstract (and in the C case you need to know *everything* about *everything* and have to "prove" it all in one go and that proof will not survive a single change) then it isn't feasible. Haskell gives you the means to manage the complexity - and grasping complexity is humanities current challenge... Neil On 28 Jul 2012, at 05:43, damodar kulkarni wrote: > > > So a language is referentially transparent if replacing a sub-term with > another with the same denotation doesn't change the overall meaning? > But then isn't any language RT with a sufficiently cunning denotational > semantics? Or even a dumb one that gives each term a distinct denotation. > > That's neat ... I mean, by performing sufficiently complicated brain > gymnastics, one can do equational reasoning on C subroutines (functions!) too. > > So, there is no "big" difference between C and Haskell when it comes to > equational reasoning... > > > Regards, > Damodar > > > On Sat, Jul 28, 2012 at 1:47 AM, Alexander Solla wrote: > > > On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson wrote: > On Fri, Jul 27, 2012 at 07:19:40PM +0100, Chris Dornan wrote: > > > So a language is referentially transparent if replacing a sub-term with > > > another with the same > > > denotation doesn't change the overall meaning? > > > > Isn't this just summarizing the distinguishing characteristic of a > > denotational semantics? > > Right, so where's the substance here? > > > My understanding is that RT is about how easy it is to carry out > > _syntactical_ transformations of a program that preserve its meaning. > > For example, if you can freely and naively inline a function definition > > without having to worry too much about context then your PL is deemed > > to possess lots of RT-goodness (according to FP propaganda anyway; note > > you typically can't freely inline function definitions in a procedural > > programming language because the actual arguments to the function may > > involve dastardly side effects; even with a strict function-calling > > semantics divergence will complicate matters). > > Ah, but we only think that because of our blinkered world-view. > > Another way of looking at it is that the denotational semanticists have > created a beautiful language to express the meanings of all those ugly > languages, and we're programming in it. > > A third way to look at it is that mathematicians, philosophers, and logicians > invented the semantics denotational semanticists have borrowed, specifically > because of the properties derived from the philosophical commitments they > made. Computer science has habit of taking ideas from other fields and > merely renaming them. "Denotational semantics" is known as "model theory" to > everyone else. > > Let's consider a referentially /opaque/ context: quotation marks. We might > say "It is necessary that four and four are eight. And we might also say > that "The number of planets is eight." But we cannot unify the two by > substitution and still preserve truth functional semantics. We would get "It > is necessary that four and four are the number of planets" (via strict > substitution joining on 'eight') or a more idiomatic phrasing like "It is > necessary that the number of planets is four and four". > > This is a big deal in logic, because there are a lot of languages which > quantify over real things, like time, possibility and necessity, etc., and > some of these are not referentially transparent. In particular, a model for > such a language will have to use "frames" to represent context, and there > typically is not a unique way to create the framing relation for a logic. > > ___ > 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
[Haskell-cafe] How to define a Monad instance
Hello. I'm trying to understand Monads. In order to do so, I decided to create my own Monad for a simple domain-specific language. The idea is to define a way to describe a multi-value replacement inside do-notation. Example of a function doing what I want (without Monads): replaceAll :: (a -> Maybe a) -> [a] -> [a] replaceAll f xs = go f xs [] where go :: (a -> Maybe a) -> [a] -> [a] -> [a] go _ [] acc = acc go f (x:xs) acc = let acc' = acc ++ [fromMaybe x (f x)] in acc' `seq` go f xs acc' Example of a replacement table: table :: Char -> Maybe Char table x = case x of 'a' -> Just 'b' 'A' -> Just 'B' _ -> Nothing Example of use: \> replaceAll table "All I want" "Bll I wbnt" Now, want I tried to do... As Monads are used for sequencing, first thing I did was to define the following data type: data TableDefinition a = Match a a (TableDefinition a) | Restart So, to create a replacement table: table' :: TableDefinition Char table' = Match 'a' 'b' (Match 'A' 'B' Restart) It look like a Monad (for me), as I can sequence any number of replacement values: table'' :: TableDefinition Char table'' = Match 'a' 'c' (Match 'c' 'a' (Match 'b' 'e' (Match 'e' 'b' Restart))) In order to run the replacement over a list, I've defined the following function: runTable :: Eq a => TableDefinition a -> [a] -> [a] runTable t = go t t [] where go _ _ acc []= acc go s Restart acc (x:xs)= let acc' = (acc ++ [x]) in acc' `seq` go s s acc' xs go s (Match a b m) acc ci@(x:xs) | x == a= let acc' = (acc ++ [b]) in acc' `seq` go s m acc' xs | otherwise = go s m acc ci The result is still the same: \> runTable table' "All I want" "Bll I wbnt" I'd like to define the same data structure as: newTable :: TableDefinition Char newTable = do 'a' :> 'b' 'A' :> 'B' But I can't figure a way to define a Monad instance for that. :( Can you help me? Thanks, Thiago. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] MonadPlus m => Maybe a -> m a
I'm solving this exercise:
http://www.haskell.org/haskellwiki/All_About_Monads#Exercise_4:_Using_the_Monad_class_constraint
I'm missing a function to transform a Maybe a into a MonadPlus m => m a.
I did search on Hoogle with no luck.
There is no standard definition for the "g" function I'm defining?
My take on the exercise:
data Sheep = Sheep {
mother :: Maybe Sheep,
father :: Maybe Sheep,
name :: String }
instance Show Sheep where -- for testing
show = name
g :: (MonadPlus m) => Maybe a -> m a
g Nothing = mzero
g (Just a) = return a
mother' :: (MonadPlus m) => Sheep -> m Sheep
mother' = g . mother
father' :: (MonadPlus m) => Sheep -> m Sheep
father' = g . father
parent'' :: (MonadPlus m) => Sheep -> m Sheep
parent'' s = mother' s `mplus` father' s
grandparent'' :: (MonadPlus m) => Sheep -> m Sheep
grandparent'' s = parent'' s >>= parent''
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] MonadPlus m => Maybe a -> m a
On Sat, Jul 28, 2012 at 8:00 AM, Thiago Negri wrote: > I'm solving this exercise: > > http://www.haskell.org/haskellwiki/All_About_Monads#Exercise_4:_Using_the_Monad_class_constraint > > I'm missing a function to transform a Maybe a into a MonadPlus m => m a. > I did search on Hoogle with no luck. > > There is no standard definition for the "g" function I'm defining? g :: (MonadPlus m) => Maybe a -> m a > g Nothing = mzero > g (Just a) = return a > I doubt there is a "standard" named function for this, since conversions between monads are typically not "unique" and there are lots and lots of pairs of monads you can convert between. You can define g in terms of Data.Maybe.maybe as: g = maybe mzero return ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] How to define a Monad instance
On 07/28/2012 03:35 PM, Thiago Negri wrote:
> [...]
As Monads are used for sequencing, first thing I did was to define the
following data type:
data TableDefinition a = Match a a (TableDefinition a) | Restart
So TableDefinition a is like [(a, a)].
[...]
>
So, to create a replacement table:
table' :: TableDefinition Char
table' =
Match 'a' 'b'
(Match 'A' 'B'
Restart)
It look like a Monad (for me), as I can sequence any number of
replacement values:
table'' :: TableDefinition Char
table'' = Match 'a' 'c'
(Match 'c' 'a'
(Match 'b' 'e'
(Match 'e' 'b'
Restart)))
Yes, but monads aren't just about sequencing. I like to see a monad as a
generalized computation (e.g. nondeterministic, involving IO, involving
state etc). Therefore, you should ask yourself if TableDefinition can be
seen as some kind of abstract "computation". In particular, can you
"execute" a computation and "extract" its result? as in
do
r <- Match 'a' 'c' Restart
if r == 'y' then Restart else Match 2 3 (Match 3 4 Restart)
Doesn't immediately make sense to me. In particular think about the
different possible result types of a TableDefinition computation.
If all you want is sequencing, you might be looking for a Monoid
instance instead, corresponding to the Monoid instance of [b], where
b=(a,a) here.
[...]
>
I'd like to define the same data structure as:
newTable :: TableDefinition Char
newTable = do
'a' :> 'b'
'A' :> 'B'
But I can't figure a way to define a Monad instance for that. :(
The desugaring of the example looks like this:
('a' :> 'b') >> ('A' :> 'B')
Only (>>) is used, but not (>>=) (i.e. results are always discarded). If
this is the only case that makes sense, you're probably looking for a
Monoid instead (see above)
-- Steffen
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Reddy on Referential Transparency
On Sat, 28 Jul 2012, damodar kulkarni wrote: So a language is referentially transparent if replacing a sub-term with another with the same denotation doesn't change the overall meaning? But then isn't any language RT with a sufficiently cunning denotational semantics? Or even a dumb one that gives each term a distinct denotation. That's neat ... I mean, by performing sufficiently complicated brain gymnastics, one can do equational reasoning on C subroutines (functions!) too. So, there is no "big" difference between C and Haskell when it comes to equational reasoning... Regards, Damodar The general theory of equational reasoning is often applicable because often we have a collection of sentences S of the form x = y where x and y are "terms", and often we have a set of models M, where given a system of backround assumptions, we can ask of the above sentence, call it s, whether in some particular model m, is it the case that eval(x) = eval(y) where now the sentence above is not a sentence of S, but rather a fact, under assumptions, about the model m, namely that what the term x means in m is equal to what the term y means in m. Here we have written what the term x refers to in m as "eval(x)". For example x might be "(vector-ref part-of-backround 17)" in some Lisp source code, given as text, and y might "(vector-ref part-of-backround 116)", and part-of-backround is some vector which comes from, in general both the model m and, this is a "scare phrase", the backround assumptions. Oi, please forgive tangle here! Note that the = in the sentence s is not the same = as in the model m, and we should in a first text write them with different symbols. As terms x and y are not equal-as-terms. It is only their "values" in m that are equal-in-m. (Obtuse Precisian Crank Further Remark: And the general theory of equality often applies to whatever sort of object lies in the vector part-of-backround at position 17, and also to whatever lies at position 116. THE ARGUMENT IS COMPLETE! But see http://iml.univ-mrs.fr/~girard/TS2.pdf for more and different.) Personal remark: I remember the wonderful feeling of having a weight lifted from me when I read this in Roger C. Lyndon's "Notes on Logic": Oi, ah, I cannot find the quote tonight. The quote was something like In this book we shall work at the level of precision which today is standard in works on the theory of groups, say. by which Lyndon meant that certain extraordinarily finicky considerations were, by the date of composition, standard, and the reader might be trusted to handle these without error. Of course, as a beginner coming to Haskell, and as an old Lisper (my first Lisp was LISP 1.5, for which see http://www.softwarepreservation.org/projects/LISP/book/LISP%201.5%20Programmers%20Manual.pdf) I wish that Haskell made more patent to my un-practiced eye more of such finicky details^Wbasics. Naturally what I'd like is Haskell source code presented in the usual parenthesized prefix notation of Lisp, with of course, every term having an immediately available complete explicit typing, which could perhaps be presented when one clicks on the term (perhaps plists might be part of the mechanism). BRING OUT THE CORE! oo--JS. On Sat, Jul 28, 2012 at 1:47 AM, Alexander Solla wrote: On Fri, Jul 27, 2012 at 12:06 PM, Ross Paterson wrote: On Fri, Jul 27, 2012 at 07:19:40PM +0100, Chris Dornan wrote: So a language is referentially transparent if replacing a sub-term with another with the same denotation doesn't change the overall meaning? Isn't this just summarizing the distinguishing characteristic of a denotational semantics? Right, so where's the substance here? My understanding is that RT is about how easy it is to carry out _syntactical_ transformations of a program that preserve its meaning. For example, if you can freely and naively inline a function definition without having to worry too much about context then your PL is deemed to possess lots of RT-goodness (according to FP propaganda anyway; note you typically can't freely inline function definitions in a procedural programming language because the actual arguments to the function may involve dastardly side effects; even with a strict function-calling semantics divergence will complicate matters). Ah, but we only think that because of our blinkered world-view. Another way of looking at it is that the denotational semanticists have created a beautiful language to express the meanings of all those ugly languages, and we're programming in it. A third way to look at it is that mathematicians, philosophers, and logicians invented the semantics denotational semanticists have borrowed, specifically because of the properties derived from the philosophical commitments they made. Computer science has habit of taking ideas from other fields and merely renaming them. "Denotational semantics" is known as "model theory" to everyone else. Let's consider a re
[Haskell-cafe] Capturing the parent element as I parse XML using parsec
Hi, With the help of the cafe I've been able to write up the xml parser using parsec - https://github.com/ckkashyap/really-simple-xml-parser/blob/master/RSXP.hs I am struggling with an idea though - How can I capture the parent element of each element as I parse? Is it possible or would I have to do a second pass to do the fixup? Regards, Kashyap ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
