Lambda the Ultimate

Actually, type checkers are theorem checkers and type inferencers are theorem reconstructors (or something like that), you start with the proof (the code) and end up with the theorem that you are proving (the type).

...and there are older threads on Why Dependent Types Matter, Djinn: A Theorem Prover in Haskell, for Haskell which also refers to Oleg Kiselyov's in-place "de-typechecker", The Reasoned Schemer (it's underappreciated, IMHO, that one of the Kanren sample applications is the Hindley-Milner type-inference relation—a typechecker, type-inferrer, and intuitionistic theorem prover all in one shot)! Also see Lightweight Static Capabilities, which has a strong dependent-type flavor but is applicable in languages such as O'Caml and Haskell today.

Here's the thread that really made it abundantly clear that my computer science education was woefully out of date and enthralled me enough to spend many hundreds of dollars on Amazon playing catch-up: Python Metaclass Programming. It contains a priceless exchange between Tim Sweeney and Frank Atanassow that is sufficient grist for years of study. See also Tim's post on Ontic, which is still something that I wish to understand some day.

Finally, see this thread on automated theorem proving, where I sing Coq and the Coq'Art book's praises, as well as reveal my own ignorance of the subject. :-)

I heartily concur; it was said somewhat tongue-in-cheek. I do like your idea of QuickCheck style presentation of instances that break the defined desired behaviour.

I do like your idea of QuickCheck style presentation of instances that break the defined desired behaviour.

to avoid the following nastiness.

Closed c;
Closed d = c;       // d is an alias for c.
Open c = c.open();  // migrates the type of c.  But what of d?

In the above pseudocode, d has type type of closed, but the underlying value has been migrated to open.

Alternatively, you need monotonic type migration--type migration is sound when a value acquires a new type which has stronger invariants then the old one--but the closed/open/closed cycle is obviously non-monotonic.

The so-called four out of five rule may come into play.

Achilleas and I had much this discussion a while back, using phantom types to encode openness/closedness, and extending to GADTs to allow sensible isOpen/isClosed predicates.

Do you have a link to that discussion? I'm interested in reading about the solution you came up with.

I think it's this thread.

Thanks, that's the one I had in mind. I don't know that my own comments were as hugely helpful as might be hoped for there.

It all sounds (a bit over my head but still) very compelling. What is the latest on that sort of thinking in terms of actually available languages? Many thanks for any refs.

Two parts (GHC) Haskell to one part Clean would get you it - I don't know off-hand of a language that has all the necessary features (anyone else?), although I imagine I could write an interpreter for an explicitly-typed intermediate lang based around System FC that handled it reasonably easily.

There's a chapter in ATTaPL on substructural type systems that covers linear types, I'm not aware of any particular interactions between them and GADTs that would prevent combining them in the obvious way.

I don't know off-hand of a language that has all the necessary features (anyone else?)

Vault can do this sort of stuff, via a linear type system.

Presumably one could do it with Coq, although I don't have much experience with it offhand.

I don't know that you could without an interpretive layer - I'm not aware of Coq supporting substructural typing directly, though I'd be happy to hear I'm wrong.

...but it'd be nice to developer a certified compiler for a language with substructural typing in Coq. :-)