Home » forums » LtU Forum

"Types and Reflection" by Lauri Emil Alanko

Types and Reflection by Lauri Emil Alanko.
If you're interested in reflection or dynamic loading in statically typed languages, this is worth reading.


One of my favorite parts of this thesis is the dynamic loading section, along with discussion of the strengths and weaknesses of Haskell's Data.Dynamic, Template Haskell, and Don Stewart's hs-plugins.

Personally, I've been trying to figure out how to get elisp quality source evaluation with Haskell, and this thesis goes a long way towards answering my outstanding questions.

By shapr at 2004-08-26 22:04 | LtU Forum | previous forum topic | next forum topic | other blogs | 17705 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Promoted to front page

I've promoted this to the front page - this paper seems like it was made for LtU. :)

By Anton van Straaten at Thu, 2004-08-26 22:52 | login or register to post comments

Looks Nice!

I'll be digging into this later this evening. Thanks for the post!

BTW, having gone way too far on the static side, let me once again point to Self. If you haven't tried it out, and you have a platform that it runs on, take it for a spin. There's an important set of lessons here about blurring "types" and "values" a la dependent types ("classes" and "objects" vs. "prototypes" in OO terminology), coupled with reflection, making some very nice direct manipulation of the computational world possible. I haven't done much beyond go through the tutorial, but that's been enough to impress me a lot.

By Paul Snively at Thu, 2004-08-26 23:12 | login or register to post comments

Typed Hardware

I haven't read the whole thing yet, but it got me to thinking that a CPU was merely an interpreter for an assembly language. Could we have a statically typed assembly language? Of course. A Harvard architecture processor has two types of bytes, code and data, and you don't ever have to worry about confusing one for the other. And protected-mode x86 has some "dynamic/latent" typing features (you can specify a virtual memory page as being read-only or read-write-execute). And you'll only find out if there are "type" errors at run-time. But modern x86 cores are actually much closer to Harvard architecture or data-path machines than von Newman machines. So has there been any other work out there on statically typed hardware? What kind of additional types should/could we have in hardware? Maybe the best way to convince the world of the greatness of static typing is to implement it in silicon (or a virtual machine?). Thoughts?

By Greg Buchholz at Fri, 2004-08-27 17:29 | login or register to post comments

Chapter 16

If lacking time for the whole paper, the 16th chapter is absolutely worth 10 minutes you will spend on it.

For one thing, it demonstrates that scientists indeed (consciously or subconsciously) use Turing machine as a synonym for program:

We can liken a process to a Turing machine, and a processor to a universal Turing machine.[...] A general-­purpose microprocessor has been intentionally designed as a universal Turing machine.

Yes, I did spot the "liken" word.

Other than that, the paper is absolutely great. It fits very nice into LtU discussion on static vs dynamic typing, "sliders", untyped and unityped.

In this sense there is no truly static safety: all program errors, type errors or otherwise, occur at some point in time. Yet type safety is rarely viewed in this light. [...] A truly static type system would have to check our brains to make sure that we won't write buggy programs [...] Indeed, a static system would have to check the genes of our parents to make sure that bad programmers were never even born. And so on.

The paper suggests a nice continuation to static vs dynamic language wars: compiled vs interpreted.

The most interesting quote might be:

But should it be possible to construct a typed language that supports reflection fully, then the language should also be able to accommodate any other programming techniques that untyped languages support. Then, hopefully, there will be less reason to avoid typed languages.
By Andris Birkmanis at Mon, 2004-08-30 07:30 | login or register to post comments

A wallaby is any macropod smaller than a kangaroo.

I read through parts of the thesis. As a survey, I found it rather interesting, but Alanko's comments on static typing and (particularly) "the fallacy of the phase distinction" are ill-informed and should not be taken for gospel.

When you see loaded phrases like "truly static type system", a red flag should go up in your head warning you that rhetoric is about to follow.

it demonstrates that scientists indeed (consciously or subconsciously) use Turing machine as a synonym for program

I would not be so hasty to generalize what appears in one student's Master's thesis.

By Frank Atanassow at Mon, 2004-08-30 15:06 | login or register to post comments

Pademelons can be distinguished from wallabies.

A wallaby is any macropod smaller than a kangaroo.
Unless it has been given some other name.

Alanko's comments on static typing and (particularly) "the fallacy of the phase distinction" are ill-informed and should not be taken for gospel.
I do not take anything for gospel, even gospel. What I do suggest is opening a mind a little bit beyond what is expressible by some formal system. If you know of sources that would enlighten us, why not share them so we are not left ill-informed?

I would not be so hasty to generalize what appears in one student's Master's thesis.
Well, "demonstrates" is weaker than "proves". I can find much more references, one of them seen just yesterday - in Concepts, Techniques, and Models of Computer Programming. Teaching students that TM are equivalent to computers might be considered just a necessary step in Wittgenstein's ladder, but I fear many students never get to throwing it away (many not necessarily being the majority).

By Andris Birkmanis at Thu, 2004-09-02 08:29 | login or register to post comments