Post by Dirk ThierbachPost by n***@motz.invalidPost by Jamie Andrews; real address @ bottom of messagePost by n***@motz.invalid"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.
Post by Dirk ThierbachI 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).
Post by n***@motz.invalidPost by Jamie Andrews; real address @ bottom of messageThat 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.
Post by n***@motz.invalidPost by Jamie Andrews; real address @ bottom of messageI'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.
Post by Dirk ThierbachPost by n***@motz.invalidAre 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.
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.