Claus Reinke wrote:
apfelmus wrote:
True enough, in a sense, a dynamically typed language is like a statically typed language with only one type (probably several by distinguishing function types) and many incomplete pattern matches. So, you can embed a dynamically typed language into a strongly typed language without loosing static type checking.
statically typed: typed at compile time dynamically typed: typed at runtime
weakly typed: .. strongly typed: everything is typed and type-checked
Ah, thanks for the clear terminology.
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.
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. Regards, apfelmus