[Haskell-cafe] small step evaluation as an unfold?

2007-01-23 Thread Steve Downey

(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 ?
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe


Re: [Haskell-cafe] small step evaluation as an unfold?

2007-01-23 Thread 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