i just noticed that i forgot to copy this message to the list..
----- Original Message -----
From: "Claus Reinke"
there are at least two problems with embedding strongly and dynamically typed languages into strongly and statically typed languages:
- it assumes that there is a globally unique static stage, entirely separate from a globally unique dynamic stage - it assumes that there is a unique, unchanging (closed) world of types
static typing alone is too static to deal with dynamically evolving types or flexible ideas such as runtime compilation or dynamic linking..
the solution is long-known as type Dynamic
Yes, that's what I meant. The "embedding" is a rather degenerate one, making everything to be of type Dynamic.
one problem is that haskell doesn't have type Dynamic. only hacked up approximations of it for monomorphic types. i don't recall whether the following is the best reference (there were many papers with similar titles), it is just the first one i find right now:
M. Abadi, L. Cardelli, B. Pierce, G. Plotkin, D. R{\`e}my, Dynamic Typing in Polymorphic Languages http://citeseer.ist.psu.edu/abadi94dynamic.html
the other problem is that there's no type registry outside of individual programs, so only programs with identical type definitions can communicate. some of the issues are discussed in 2003: 6. Martijn Vervoort and Rinus Plasmeijer. Lazy Dynamic Input/Output in the lazy functional language Clean http://www.st.cs.ru.nl/Onderzoek/Publicaties/publicaties.html
some more discussion in earlier publications on orthogonal persistent systems. the only losely related one i can find right now is
Connor, RCH, Cutts, QI, Kirby, GNC, Morrison, R, Using Persistence Technology to Control Schema Evolution http://www-old.cs.st-andrews.ac.uk/research/publications/CCK+94a.php
where "schema evolution" is the database community term for what is the evolution of type definitions in an orthogonally persistent language (another thing haskell doesn't address: try compiling old -previously type-correct!- haskell code with new ghc/libraries where the library types and apis have changed..; the static typing of haskell only ever addresses fragments of the lifetime of programs and data - between these fragments, we're back to untyped strings/object code; so when i say i want Dynamics, i don't want to weaken the type system, i want to extend its range - more safety, not less;-).
[that paper also happens to feature some screenshots of an ide that permits program parts expressed as source text to refer to program parts that have already been run and stored, a kind of hyperlinked program representation which might be of independent interest;-]
imagine a language that can implement something like an advanced hs-plugins: at runtime of program A, a string representing program B, including new type definitions and code, is type checked, compiled, and linked into the running program A, so that entities in A and B can interact as if they'd been written as parts of a single program.
the "static" type-checking of B is a "dynamic" type-check if viewed from A. and if the contents of B are not known when A is compiled, there's no way of writing down a universal sum type in A that usefully encompasses all the possible types in B as well. at least not in current haskell.
if you have a strongly and dynamically typed language, you can embed strongly and statically typed languages into it. by default, that means you get more type-checks than necessary and type-errors later than you'd wish, but you still get them. eliminating runtime type information and runtime type-checks in a strongly and dynamically typed language is a question of optimisation, similar to deforestation.
Well, you can't embed the static checks into dynamic checks without loosing the fact that they're static. Which I think is the crucial point: "program testing can be used very effectively to show the presence of [type] bugs but never to show their absence." To me, dynamic typing is next to useless, i want a (partial) proof that the program works since a proof is really the only way to know whether it works.
yes, and no. no, because there's nothing keeping the dynamically typed system from doing as many type-checks as early as possible; yes, because there's nothing in the dynamically typed language that says "i want all my type-checks to be done before this point, and a guarantee that no type-errors can occur after this point", so the dynamically typed system can't really report the errors until just before their execution.
so, you're right. Dynamic and typecase are necessary extensions not just to strongly and statically typed languages but also to strongly and dynamically typed languages. in the former, they extend the set of expressible programs, in the latter, they extend the set of expressible restrictions/safety checks.
i don't want dynamically typed or statically typed languages, i want the safety of static types whereever possible, combined with the expressiveness of dynamic types only where needed. and one known way of expressing the phase shift between dynamic and static typing precisely and safely are Dynamic/ typecase:
- in an otherwise statically typed language, they permit me to write programs that couldn't be expressed otherwise
- in an otherwise dynamically typed language, they permit me to extend type-safety over whole regions of code at once in ways that couldn't be expressed otherwise
claus