[Haskell-cafe] Re: Best idiom for avoiding Defaulting warnings with ghc -Wall -Werror ??

[apfelmus]

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