<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
<meta content="text/html;charset=ISO-8859-1" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
Duncan Coutts wrote:
<blockquote cite="mid1115285084.10126.23.camel@localhost" type="cite">
<pre wrap="">On Wed, 2005-05-04 at 18:29 -0400, Jacques Carette wrote:
</pre>
<blockquote type="cite">
<pre wrap="">There is also Template Haskell vs MetaOCaml.
For the life of me, I still cannot fathom why Template Haskell is untyped, while MetaOCaml is fully typed. Which is
the main reason I write meta-program in MetaOCaml and 'other' programs in Haskell.
</pre>
</blockquote>
<pre wrap="">
The reason for this is that Template Haskell is more powerful and
correspondingly harder to type so it is currently untyped.
</pre>
</blockquote>
``more powerful'' meaning that it can do some level of introspection,
right? I know introspection can be very powerful (I designed Maple's
modern reflection and reification facilities...), but I was under the
impression that type systems that can handle 'too much' introspection
were unsound [a result of Walid Taha].<br>
<blockquote cite="mid1115285084.10126.23.camel@localhost" type="cite">
<pre wrap="">The main reason it is more porwerful is that TH allows you to pattern
match on the abstract syntax of a quoted expression and perform
arbitrary transformations on that. It would be hard to preserve the
well-typedness of the AST and still allow arbitrary transformations.
</pre>
</blockquote>
Can't this be regarded as a 'convenience' rather than as actual extra
power? Using an abstract interpretation formalism (see papers of Taha
and co-authors), it is possible to 'lift' the type of code values into
staging-time terms, and pattern-match on that instead. Then
well-typedness of transformations is much easier to show. In this way
one can even implement some transformations that are equivalent to what
are currently 'hints' to GHC as well-typed code [I have some code that
does this, but there are only hints of this in a preprint of mine --
see the conclusion section of "<a
href="http://www.cas.mcmaster.ca/%7Ecarette/publications/ge.pdf"><b>Gaussian
Elimination: a case study in efficient genericity with MetaOCaml"</b> </a>available
from <a class="moz-txt-link-freetext" href="http://www.cas.mcmaster.ca/~carette/publications.html">http://www.cas.mcmaster.ca/~carette/publications.html</a> for some
hints on how this is done<br>
<blockquote cite="mid1115285084.10126.23.camel@localhost" type="cite">
<pre wrap="">A colleague of mine is currently developing a type system for Template
Haskell that should catch most errors without restricting too much the
programs you can write.
</pre>
</blockquote>
I am eagerly awaiting this! Writing Monadic meta-programs in MetaOCaml
is feasible, but the lack of native support for Monads makes it
significantly harder. But after spending 12 years writing programs in
a fully dynamically typed language (Maple), I am much happier writing <b>all
</b>parts of my programs in a strongly typed language!<br>
<br>
Jacques<br>
</body>
</html>