OP wrote:
> "The Design of a Pretty Printing Library", by John Hughes.
> (http://citeseer.ist.psu.edu/hughes95design.html) He begins
> with a simple design and elaborates it through algebraic
> transformations of the Haskell source code until he arrives
> at a sophisticated, efficient design. The final product is
> related to the initial product through these transformations.
OK, I finally got the *.ps file [which is one of those where
I can't auto-extract any of the ascii, by eg. 'pdftotext',
which is strange, since it's generated from Latex and not just
a photo of a typed paper ?], and am very well impressed.
But I don't want to learn Haskell - yet another syntax !
And since google shows there are some scheme ports of this
famous work, and I have some familiarity with scheme, I was
wondering if the theoretical aspects of, as J.Hughes writes:
"use formal specification of the combinators, and a study of their
algebraic properties, to guide both the design and implementation
of a combinator library", can be found/done via scheme ?
A mere scheme port of the haskell code, won't help me, because
I want to get a full understanding of the theoretical steps
which J. Hughes shows in his 41 page paper.
Can I get a full understanding of algebraic transformations of
combinators via scheme ?
== TIA.
On Apr 30, 3:33 am, ··········@motz.invalid wrote:
> I was wondering if the theoretical aspects of, as J.Hughes writes:
> "use formal specification of the combinators, and a study of their
> algebraic properties, to guide both the design and implementation
> of a combinator library", can be found/done via scheme ?
You may find the formatting library by Alex Shinn interesting:
http://synthcode.com/scheme/fmt/
From: Jamie Andrews; real address @ bottom of message
Subject: Re: Haskell formal transformations via scheme ?
Date:
Message-ID: <7613d0F1ao6rdU1@mid.individual.net>
In comp.theory ··········@motz.invalid wrote:
>> "The Design of a Pretty Printing Library", by John Hughes.
>> (http://citeseer.ist.psu.edu/hughes95design.html)
> A mere scheme port of the haskell code, won't help me, because
> I want to get a full understanding of the theoretical steps
> which J. Hughes shows in his 41 page paper.
> Can I get a full understanding of algebraic transformations of
> combinators via scheme ?
That paper has a lot to do with monads. Monads are a
non-trivial construction in typed higher order logic. I'm not
sure whether they are representable (or worthwhile to represent)
in a language like Scheme.
--Jamie. (efil4dreN)
andrews .uwo } Merge these two lines to obtain my e-mail address.
@csd .ca } (Unsolicited "bulk" e-mail costs everyone.)
Jamie Andrews; real address @ bottom of message escreveu:
> In comp.theory ··········@motz.invalid wrote:
>>> "The Design of a Pretty Printing Library", by John Hughes.
>>> (http://citeseer.ist.psu.edu/hughes95design.html)
>> A mere scheme port of the haskell code, won't help me, because
>> I want to get a full understanding of the theoretical steps
>> which J. Hughes shows in his 41 page paper.
>> Can I get a full understanding of algebraic transformations of
>> combinators via scheme ?
>
> That paper has a lot to do with monads. Monads are a
> non-trivial construction in typed higher order logic. I'm not
> sure whether they are representable (or worthwhile to represent)
> in a language like Scheme.
http://groups.google.com/group/comp.lang.functional/msg/2fde5545c6657c81
and the whole discussion that prompted it
and:
http://okmij.org/ftp/Scheme/monad-in-Scheme.html
They come from the top results in Google for "monads in Scheme" ;)
Anyway, indeed not much use in a language with imperative constructs
builtin and no static typing.
--
a game sig: http://tinyurl.com/d3rxz9
From: ··········@motz.invalid
Subject: Re (2): Haskell formal transformations via scheme ?
Date:
Message-ID: <gttidl$1er$1@news.motzarella.org>
In article <···············@mid.individual.net>, ··@privacy.net (Jamie Andrews; real address @ bottom of message) wrote:
> In comp.theory ··········@motz.invalid wrote:
> >> "The Design of a Pretty Printing Library", by John Hughes.
> >> (http://citeseer.ist.psu.edu/hughes95design.html)
> > A mere scheme port of the haskell code, won't help me, because
> > I want to get a full understanding of the theoretical steps
> > which J. Hughes shows in his 41 page paper.
> > Can I get a full understanding of algebraic transformations of
> > combinators via scheme ?
>
> That paper has a lot to do with monads. Monads are a
> non-trivial construction in typed higher order logic. I'm not
> sure whether they are representable (or worthwhile to represent)
> in a language like Scheme.
>
> --Jamie.
That's bad new, because it implies that the 'algebraic
transformations of combinators' ...etc. as a formal method,
is only applicable with Haskell.
But since all languages are Turin(?sp)-equivalent, so eg.
OO techniques can be simulated in any language.
Are you familiar with the paper to the extent that you can
say it does show step-wise algebraic trnsformations from
a specification to an implementation ?
Thanks for any fedback,
== Chris Glur.
Although this NewsGroup still functions well,
there are already many other previously good
NewsGroups which have been crowed-out by
the twittering-idiot-masses. To avoid further
displacement of the NNT-protocol by the
dumbed-down inefficient clik-blogs, we need
to take a stand.
··········@motz.invalid wrote:
> ··@privacy.net (Jamie Andrews; real address @ bottom of message) wrote:
>> In comp.theory ··········@motz.invalid wrote:
>> >> "The Design of a Pretty Printing Library", by John Hughes.
>> >> (http://citeseer.ist.psu.edu/hughes95design.html)
>> > A mere scheme port of the haskell code, won't help me, because
>> > I want to get a full understanding of the theoretical steps
>> > which J. Hughes shows in his 41 page paper.
>> > Can I get a full understanding of algebraic transformations of
>> > combinators via scheme ?
IMHO the language doesn't really play a role. What you need are
algebraic data types and some idea why one can transform pure
expressions without being afraid of making semantic changes.
I guess one could get "a full understanding" of that in Scheme as well.
But since the paper uses Haskell as notation, it probably doesn't hurt
to learn that bits and pieces of Haskell syntax that are required
(it doesn't appear to be much; a basic introduction into Haskell
should be sufficient).
>> That paper has a lot to do with monads. Monads are a
>> non-trivial construction in typed higher order logic.
Actually, once you get used to them, they are pretty simple. Just
don't get irritated by that scary name. And you don't need to understand
the theory (more category theory than higher order logic) at all
to be able to use them.
And unless I'm mistaken, the implementation of that paper that
made it into the Haskell standard library doesn't use monads at all,
so I wouldn't really say "this paper has a lot to do with monads".
I only skimmed over the paper, so I may be wrong, but I don't see any
monads used there in the pretty printing part either, hence I think he
mentions them just as an example of the technique.
>> I'm not sure whether they are representable (or worthwhile to
>> represent) in a language like Scheme.
Googling for "monads scheme lisp" finds 14.000 hits, including for
example
http://www.ccs.neu.edu/home/dherman/research/tutorials/monads-for-schemers.txt
> That's bad new, because it implies that the 'algebraic
> transformations of combinators' ...etc. as a formal method,
> is only applicable with Haskell.
Of course not. It's applicable to every language.
> Are you familiar with the paper to the extent that you can
> say it does show step-wise algebraic trnsformations from
> a specification to an implementation ?
As I said, I only skimmed over the paper, but I'd say the gist is that
he moves from algebraic laws (i.e. equational specification) for layout
(section 7.2) to a term representation (section 8) by choosing which
"atoms" to use as constructors, and then figuring out the rest by case
analysis on the constructors so that the laws hold. The remaining
stuff is mainly details how to get the pretty printing right.
That's a standard approach. If you aren't used to it, maybe it's
more helpful to look at smaller example of an equational specification
or algebraic specification first (say, stacks). I tried a quick
googling for a good tutorial, but didn't find anything that really
satisfied me. The best I found so far is
http://www.comp.lancs.ac.uk/computing/resources/IanS/SE7/ElectronicSupplements/AlgebraicSpec.pdf
which at least has enough examples, though it probably goes into more details
than you need. Maybe reading it helps.
- Dirk
From: ·······@gmail.com
Subject: Re (3): Haskell formal transformations via scheme ?
Date:
Message-ID: <gu1ojc$kmd$1@news.motzarella.org>
In article <····························@dthierbach.news.arcor.de>, Dirk Thierbach <··········@usenet.arcornews.de> wrote:
> ··········@motz.invalid wrote:
> > ··@privacy.net (Jamie Andrews; real address @ bottom of message) wrote:
>
> >> In comp.theory ··········@motz.invalid wrote:
> >> >> "The Design of a Pretty Printing Library", by John Hughes.
> >> >> (http://citeseer.ist.psu.edu/hughes95design.html)
>
> >> > A mere scheme port of the haskell code, won't help me, because
> >> > I want to get a full understanding of the theoretical steps
> >> > which J. Hughes shows in his 41 page paper.
> >> > Can I get a full understanding of algebraic transformations of
> >> > combinators via scheme ?
>
> IMHO the language doesn't really play a role. What you need are
> algebraic data types and some idea why one can transform pure
> expressions without being afraid of making semantic changes.
>
Yes, that's what I'm hoping for.
> I guess one could get "a full understanding" of that in Scheme as well.
> But since the paper uses Haskell as notation, it probably doesn't hurt
> to learn that bits and pieces of Haskell syntax that are required
> (it doesn't appear to be much; a basic introduction into Haskell
> should be sufficient).
>
> >> That paper has a lot to do with monads. Monads are a
> >> non-trivial construction in typed higher order logic.
>
> Actually, once you get used to them, they are pretty simple. Just
> don't get irritated by that scary name. And you don't need to understand
> the theory (more category theory than higher order logic) at all
> to be able to use them.
>
> And unless I'm mistaken, the implementation of that paper that
> made it into the Haskell standard library doesn't use monads at all,
> so I wouldn't really say "this paper has a lot to do with monads".
>
> I only skimmed over the paper, so I may be wrong, but I don't see any
> monads used there in the pretty printing part either, hence I think he
> mentions them just as an example of the technique.
>
> >> I'm not sure whether they are representable (or worthwhile to
> >> represent) in a language like Scheme.
>
> Googling for "monads scheme lisp" finds 14.000 hits, including for
> example
>
> http://www.ccs.neu.edu/home/dherman/research/tutorials/monads-for-schemers.txt
>
Ok, I fetched that for reading.
>
> > Are you familiar with the paper to the extent that you can
> > say it does show step-wise algebraic trnsformations from
> > a specification to an implementation ?
>
> As I said, I only skimmed over the paper, but I'd say the gist is that
> he moves from algebraic laws (i.e. equational specification) for layout
> (section 7.2) to a term representation (section 8) by choosing which
> "atoms" to use as constructors, and then figuring out the rest by case
> analysis on the constructors so that the laws hold. The remaining
> stuff is mainly details how to get the pretty printing right.
>
> That's a standard approach. If you aren't used to it, maybe it's
> more helpful to look at smaller example of an equational specification
> or algebraic specification first (say, stacks). I tried a quick
> googling for a good tutorial, but didn't find anything that really
> satisfied me. The best I found so far is
>
> http://www.comp.lancs.ac.uk/computing/resources/IanS/SE7/
> ElectronicSupplements/AlgebraicSpec.pdf
>
> which at least has enough examples, though it probably goes into more details
> than you need. Maybe reading it helps.
>
Yes, he uses a 'schema/notation' with 4 parts [which reminds
me of "Z"], and for his chosen example
] consider the specification of an array..
and describes the 3rd part as:
[ Operation signatures & names/types of pars
[ Create (Integer, Integer) -> Array
[ Assign (Array, Integer, Elem) -> Array
[ First (Array) -> Integer
[ Last (Array) -> Integer
[ Eval (Array, Integer) -> Elem
which seems a pretty intuitive set of functions.
But then for the 4th part, he's got these :-
] Axioms defining the operations over the sort
[ First (Create (x, y)) = x
[ First (Assign (a, n, v)) = First (a)
[ Last (Create (x, y)) = y
[ Last (Assign (a, n, v)) = Last (a)
[ Eval (Create (x, y), n) = Undefined
[ Eval (Assign (a, n, v), m) =
[ if m < First (a) or m > Last (a) then Undefined else
[ if m = n then v else Eval (a, m)
which although they may be true, aren't clear why
they are chosen as the axioms, any more than:
"5 is the (successor(successor)) of 3"
should qualify as an axiom.
I believe that a chosen set of axioms must 'cover the domain'.
I can't see this getting me to my hoped-for destination:
an *algorithm* to write specifications and transform them to
valid code.
Well not exactly an algorithm, else the machine could write
the code. But at least I need some heuristic guidance.
> - Dirk
Thanks for feedback. I'll try more to see the light....
== Chris Glur.
Although this NewsGroup still functions well,
there are already many other previously good
NewsGroups which have been crowed-out by
the twittering-idiot-masses. To avoid further
displacement of the NNT-protocol by the
dumbed-down inefficient clik-blogs, we need
to take a stand.
·······@gmail.com wrote:
> Dirk Thierbach <··········@usenet.arcornews.de> wrote:
>> Googling for "monads scheme lisp" finds 14.000 hits, including for
>> example
>> http://www.ccs.neu.edu/home/dherman/research/tutorials/monads-for-schemers.txt
> Ok, I fetched that for reading.
Didn't look at it in detail though, there may be better ones.
> Yes, he uses a 'schema/notation' with 4 parts [which reminds
> me of "Z"], and for his chosen example
> ] consider the specification of an array..
> and describes the 3rd part as:
> [ Operation signatures & names/types of pars
> [ Create (Integer, Integer) -> Array
> [ Assign (Array, Integer, Elem) -> Array
> [ First (Array) -> Integer
> [ Last (Array) -> Integer
> [ Eval (Array, Integer) -> Elem
> which seems a pretty intuitive set of functions.
> But then for the 4th part, he's got these :-
> ] Axioms defining the operations over the sort
> [ First (Create (x, y)) = x
> [ First (Assign (a, n, v)) = First (a)
> [ Last (Create (x, y)) = y
> [ Last (Assign (a, n, v)) = Last (a)
> [ Eval (Create (x, y), n) = Undefined
> [ Eval (Assign (a, n, v), m) =
> [ if m < First (a) or m > Last (a) then Undefined else
> [ if m = n then v else Eval (a, m)
> which although they may be true, aren't clear why
> they are chosen as the axioms, any more than:
> "5 is the (successor(successor)) of 3"
> should qualify as an axiom.
> I believe that a chosen set of axioms must 'cover the domain'.
Yes. The trick that usually works is to identify some of the
operations as "constructors" (meaning that all possible values of the
datatype can be constructed usem them alone). Then, for each of
the other functions (also called "value-operations"), apply them
to all constructors in turn and see if one can come up with an
equation that "simplifies" the expression.
In the above example, that is exactly what happens: Create and Assign
are the constructors, so for the equations, one looks at
First (Create (...)) and First (Assign (...)), then at
Last (Create (...)) and Last (Assign (...)), and so on.
That doesn't always work smoothly, sometimes one has to add side
conditions (as above), or one has to make more complicated case
distinctions.
If you haven't already read about it, a good exercise is to try that
first with a stack, and then with a queue.
> I can't see this getting me to my hoped-for destination:
> an *algorithm* to write specifications and transform them to
> valid code.
> Well not exactly an algorithm, else the machine could write
> the code. But at least I need some heuristic guidance.
As a heuristic, the above method works usually well. It's also very
easy to implement such a specification in Haskell, because the
algebraic datatype consists just of the constructors, and with pattern
matching one can write down the other functions in nearly exactly the
same way as the equations above.
- Dirk
In article <············@news.motzarella.org>, ·······@gmail.com wrote:
> In article <····························@dthierbach.news.arcor.de>, Dirk
> Thierbach <··········@usenet.arcornews.de> wrote:
>
> > ··········@motz.invalid wrote:
> > > ··@privacy.net (Jamie Andrews; real address @ bottom of message) wrote:
> >
> > >> In comp.theory ··········@motz.invalid wrote:
> > >> >> "The Design of a Pretty Printing Library", by John Hughes.
> > >> >> (http://citeseer.ist.psu.edu/hughes95design.html)
> >
> > >> > A mere scheme port of the haskell code, won't help me, because
> > >> > I want to get a full understanding of the theoretical steps
> > >> > which J. Hughes shows in his 41 page paper.
> > >> > Can I get a full understanding of algebraic transformations of
> > >> > combinators via scheme ?
> >
> > IMHO the language doesn't really play a role. What you need are
> > algebraic data types and some idea why one can transform pure
> > expressions without being afraid of making semantic changes.
> >
> Yes, that's what I'm hoping for.
>
> > I guess one could get "a full understanding" of that in Scheme as well.
> > But since the paper uses Haskell as notation, it probably doesn't hurt
> > to learn that bits and pieces of Haskell syntax that are required
> > (it doesn't appear to be much; a basic introduction into Haskell
> > should be sufficient).
> >
> > >> That paper has a lot to do with monads. Monads are a
> > >> non-trivial construction in typed higher order logic.
> >
> > Actually, once you get used to them, they are pretty simple. Just
> > don't get irritated by that scary name. And you don't need to understand
> > the theory (more category theory than higher order logic) at all
> > to be able to use them.
> >
> > And unless I'm mistaken, the implementation of that paper that
> > made it into the Haskell standard library doesn't use monads at all,
> > so I wouldn't really say "this paper has a lot to do with monads".
> >
> > I only skimmed over the paper, so I may be wrong, but I don't see any
> > monads used there in the pretty printing part either, hence I think he
> > mentions them just as an example of the technique.
> >
> > >> I'm not sure whether they are representable (or worthwhile to
> > >> represent) in a language like Scheme.
> >
> > Googling for "monads scheme lisp" finds 14.000 hits, including for
> > example
> >
> > http://www.ccs.neu.edu/home/dherman/research/tutorials/monads-for-schemers.t
> > xt
> >
> Ok, I fetched that for reading.
> >
> > > Are you familiar with the paper to the extent that you can
> > > say it does show step-wise algebraic trnsformations from
> > > a specification to an implementation ?
> >
> > As I said, I only skimmed over the paper, but I'd say the gist is that
> > he moves from algebraic laws (i.e. equational specification) for layout
> > (section 7.2) to a term representation (section 8) by choosing which
> > "atoms" to use as constructors, and then figuring out the rest by case
> > analysis on the constructors so that the laws hold. The remaining
> > stuff is mainly details how to get the pretty printing right.
> >
> > That's a standard approach. If you aren't used to it, maybe it's
> > more helpful to look at smaller example of an equational specification
> > or algebraic specification first (say, stacks). I tried a quick
> > googling for a good tutorial, but didn't find anything that really
> > satisfied me. The best I found so far is
> >
> > http://www.comp.lancs.ac.uk/computing/resources/IanS/SE7/
> > ElectronicSupplements/AlgebraicSpec.pdf
> >
> > which at least has enough examples, though it probably goes into more
> > details
> > than you need. Maybe reading it helps.
> >
> Yes, he uses a 'schema/notation' with 4 parts [which reminds
> me of "Z"], and for his chosen example
> ] consider the specification of an array..
> and describes the 3rd part as:
> [ Operation signatures & names/types of pars
> [ Create (Integer, Integer) -> Array
> [ Assign (Array, Integer, Elem) -> Array
> [ First (Array) -> Integer
> [ Last (Array) -> Integer
> [ Eval (Array, Integer) -> Elem
> which seems a pretty intuitive set of functions.
> But then for the 4th part, he's got these :-
> ] Axioms defining the operations over the sort
> [ First (Create (x, y)) = x
> [ First (Assign (a, n, v)) = First (a)
> [ Last (Create (x, y)) = y
> [ Last (Assign (a, n, v)) = Last (a)
> [ Eval (Create (x, y), n) = Undefined
> [ Eval (Assign (a, n, v), m) =
> [ if m < First (a) or m > Last (a) then Undefined else
> [ if m = n then v else Eval (a, m)
> which although they may be true, aren't clear why
> they are chosen as the axioms, any more than:
> "5 is the (successor(successor)) of 3"
> should qualify as an axiom.
On p 10.6 he says:
A good rule of thumb for writing an algebraic specification is
to establish he constructor operations and write down an axiom
for each inspection operation over each constructor.
This suggests that if there are m constructor operations and n
inspection operations there should be m*n axioms defined.
> I believe that a chosen set of axioms must 'cover the domain'.
>
> I can't see this getting me to my hoped-for destination:
> an *algorithm* to write specifications and transform them to
> valid code.
One method of transforming an algebraic spec into a set of rewrite rules
is "Knuth-Bendix completion". See
<http://en.wikipedia.org/wiki/Knuth-Bendix_completion_algorithm>.
> Well not exactly an algorithm, else the machine could write
> the code. But at least I need some heuristic guidance.
>
> > - Dirk
>
> Thanks for feedback. I'll try more to see the light....
--
---------------------------
| BBB b \ Barbara at LivingHistory stop co stop uk
| B B aa rrr b |
| BBB a a r bbb | Quidquid latine dictum sit,
| B B a a r b b | altum viditur.
| BBB aa a r bbb |
-----------------------------