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

[Claus Reinke]

i just noticed that i forgot to copy this message to the list..

----- Original Message ----- 
From: "Claus Reinke" <claus.reinke at talk21.com>
To: "apfelmus" <apfelmus at quantentunnel.de>
Sent: Monday, June 25, 2007 12:20 PM
Subject: Re: [Haskell-cafe] Re: Best idiom for avoiding Defaulting warnings with ghc -Wall -Werror 
??


>>> 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
>