On Sat, 25 Aug 2012, Kristopher Micinski <krismicin...@gmail.com> wrote:
I do not know Haskell. It looks to me as though there are
several pieces of the mechanism:
1. There is, once the extensions are specified, a particular Type
System, that is, a formal system with, on the syntactic side, at
least, assumptions, judgements, rules of inference, terms lying
in some lambda calculus, etc..
That's right. Extensions get complex too, however, and can't be
necessarily easily dismissed (not to imply you were doing so),
RankNTypes, for example,
I suspected that some of these extensions might cause Haskell
expressions to be hard to type. One thing I am not clear on is
whether any standard extensions require modifications to
(internal) Core.
2. The Type Inference Subsystem, which using some constraint
solver calculates the type to be assigned to the value of Haskell
expressions.
Yes, that's right, for core haskell this is typically damas milner
(let bound) polymorphism
Ah, yes, thank you. I almost believe in Hindley-Damas-Milner but
have not yet attempted the standard initiation course.
3. The machine which does "reduction", perhaps "execution", on
the value of Haskell expressions. This is, by your account, the
STG machine.
Yes, notably graph reduction allows sharing, which is an important
part of Haskell's semantics,
Ah, thanks!
There is a textual version of Haskell's Core. If it were
executable and the runtime were solid and very simple and clear
in its design, I think we would have something close to a "formal
semantics". We'd also require that the translation to STG code
be very simple.
Yes, that's right. The translation to STG (or something like it,
another core language) can be found in many books and articles,
This is good. I will look at the references given in this
thread. The account at
http://web.archive.org/web/20060206074101/http://www.cse.ogi.edu/~mpj/thih/TypingHaskellInHaskell.html
is, I think, one part of what I was looking for.
But others here have also specified some good references for
executable versions of Core. Still unsure if the translation from
Haskell to Core has been verified, I would suspect not, as I haven't
heard of any such thing.
kris
This part of the project I am less interested in, due to my fear,
I am an old Lisper, that the luxuriant syntactic undergrowth
might be hard to hack through. If we had an executable Core,
which might have to be extended (after perhaps some subtraction)
with a simple notation for type annotations, and the rest of the
apparatus, I think this would be very useful. Even though we
would not gain one of the claimed advantages of
rigor-all-the-way, that is, better bug suppression for ordinary
Haskell as she is spoke.
oo--JS.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
