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
