small step evaluation as an unfold?
(overall context - working through TaPL on my own, reimplemnting typecheckers in haskell) the type checkers all follow the same pattern, in ocaml they throw an exception when the small step fails, which may mean taking another branch in the eval, but that that sub expression has hit bottom. it is self admittedly not good ocaml, and it seems to be even worse haskell, as i try to extend the simple evaluator i have to deal with managing reporting errors. having the single small step evaluator return a Maybe is fairly close. then the evaluator above it just bottoms out when eval1 expr returns Nothing, by passing expr back up as the result. but it occurs to me that it might be better to express it as an unfold, where the result is a list with the last element as the irresucible expression. or am i insane / intoxicated ?
On Tue, Jan 23, 2007 at 10:25:27PM -0500, Steve Downey wrote:
(overall context - working through TaPL on my own, reimplemnting typecheckers in haskell) the type checkers all follow the same pattern, in ocaml they throw an exception when the small step fails, which may mean taking another branch in the eval, but that that sub expression has hit bottom.
it is self admittedly not good ocaml, and it seems to be even worse haskell, as i try to extend the simple evaluator i have to deal with managing reporting errors.
having the single small step evaluator return a Maybe is fairly close. then the evaluator above it just bottoms out when eval1 expr returns Nothing, by passing expr back up as the result.
but it occurs to me that it might be better to express it as an unfold, where the result is a list with the last element as the irresucible expression.
you would probably be interested in the helium type checker, which is designed to give excellent error messages above all else. Basically, what it does (up to my understanding) is perform a standard type-inference traversal of your code, but rather than unify things as it comes to them, it collects a set of constraints of what to unify with what. then, once they are all collected, it can use a variety of constraint solving techniques, whichever produces the best messages. it even allows users to annotate their routines with specialized constraint solving strategies and type error messages. it is really quite neat. http://www.cs.uu.nl/helium/documentation.html John -- John Meacham - ⑆repetae.net⑆john⑈
I'll take a look at that, since one of the next things on my list is
error propagation and reporting.
In Pierce's code, source information is carried through as an explict
part of the type that represents terms in the language. I think that
would be more naturally expressed in a monad transformer, so that the
concerns of expression and type evaluation are separated from error
reporting.
But best to leave the next problem for next.
It was actually the discussion here about ListT being equivalent to a
pair of a and a Maybe of the type. So that [] is equivalent to
Nothing. Which have always seemed related, but I wasn't sure how.
Seeing that, though made me realize that expressing the evaluation as
an unfold, with the term I'm currently returning as the last element,
might make other compositions easier to write, and to follow the chain
of deductions being made.
Now I just have to write it.
On 1/23/07, John Meacham
On Tue, Jan 23, 2007 at 10:25:27PM -0500, Steve Downey wrote:
(overall context - working through TaPL on my own, reimplemnting typecheckers in haskell) the type checkers all follow the same pattern, in ocaml they throw an exception when the small step fails, which may mean taking another branch in the eval, but that that sub expression has hit bottom.
it is self admittedly not good ocaml, and it seems to be even worse haskell, as i try to extend the simple evaluator i have to deal with managing reporting errors.
having the single small step evaluator return a Maybe is fairly close. then the evaluator above it just bottoms out when eval1 expr returns Nothing, by passing expr back up as the result.
but it occurs to me that it might be better to express it as an unfold, where the result is a list with the last element as the irresucible expression.
you would probably be interested in the helium type checker, which is designed to give excellent error messages above all else. Basically, what it does (up to my understanding) is perform a standard type-inference traversal of your code, but rather than unify things as it comes to them, it collects a set of constraints of what to unify with what. then, once they are all collected, it can use a variety of constraint solving techniques, whichever produces the best messages. it even allows users to annotate their routines with specialized constraint solving strategies and type error messages. it is really quite neat.
http://www.cs.uu.nl/helium/documentation.html
John
-- John Meacham - ⑆repetae.net⑆john⑈ _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
participants (2)
-
John Meacham -
Steve Downey