Lambda the Ultimate

[nm]

But AI is not some kind of magic bullet. To use it in the types of examples in the paper it is still necessary to define abstract domains in such a way that the analysis can terminate with a sufficiently precise value. For complex domains this becomes quite a substantial programming task and the question that naturally arises is how to express those conversions and the rules for abstract analysis.

In short, you'd need some kind of extension to the syntax and semantics of a language to really support AI as a system for proving static properties. Without designing such a system it is kind of hard to say whether or not it would look as elegant as Omega. It also seems worth noting that the computations over kinds / types are already a form of AI for the lower layers in their hierarchy.

After a quick skim through the paper: wow! This does look very nice. We used dependent types a while ago to model quite a complex domain, and as the system became more and more precise we ended up writing larger and more complex mappings over the type parameters. In the end we used a small constraint language to make things work, the approach in Omega seems a lot more elegant and complete.

Oh, I know it's not a magic bullet, my point was simply that AI has a lot of unexplored potential. The push towards making dependent types more friendly is great, but we shouldn't ignore other possible avenues.

Types give a kind of abstract interpretation. And many kinds of abstract interpretation can be achieved nicely by appropriate use of types.

This reminds me of the paper by Cousot: Types as Abstract Interpretations

The LtU thread discussing this, and other papers on AI and type checking.

As for types vs. abstraction interpretations, yes types would be involved even a language using AI, and type checking and AI are formally connected. However, a type system weaker than dependent types inherently limits you in the properties it can prove.

The paper on Near-concrete Program Interpretation is designed to gather and export the value bindings generated from an abstract interpretation of a program, including values generated using general recursion, so that they can be imported into a theorem prover, and even more powerful properties of a program can be reasoned about.

This single, uniform analysis further permits flow, context and path sensitive analyses. I'm not aware of any single type system that allows this breadth of analysis, particularly in the presence of general recursion.

Thanks for the insightful comment and links! What I find so attractive about Omega is its parsimony of concepts: anyone who understands generics at some depth can understand the basics of Omega. IMO Omega is so great in that it shows the power of Curry-Howard in such a simple setting. Solving pragmatic issues, such as the code reuse you mention, may well demand a lot more work, but that doesn't detract from Omega's eye-opening power. GADTs + Extensible Kinds seems to me like a "local optimum", where some benefits of dependent programming can be had, without literally requiring a PhD.

I agree completely. What's to follow is all pretty hand-wavy, so please excuse the quotes.

I think another way of solving the reusability problem might be to start by looking at the way people are proposing to interface statically typed languages to dynamic ones (see, e.g., Well-typed Programs Can't be blamed), and adapting it to interfacing "less statically" typed languages to "fully dependently" typed languages, or, rather, in the same language: something like extending subtyping to allow upcasting ("approximating"/generalising) code that is "too precise" for reuse.

Of course, the need for casts is usually an indication of a lack of polymorphism, so, rather than casting away the precision, maybe we should allow polymorphism in the "precision" of these proofs, or the proofs themselves, or something else :-) (which, I guess relates to your paragraph about the Generic chapter in CPDT).

Strong normalization is useful for logical soundness, not for some kind of practical guarantees about actual evaluation.

I'm not sure how often it matters at the type level, but in a total language, it's not necessary to evaluate terms with types like "Equal a b" at all - the only reason a language with general recursion has to evaluate such a term and perhaps thereby fall into an infinite loop is because it allows infinite loops, so it has to evaluate the term to be sure it's really an equality proof and not just an infinte loop.

Here's a modest example showing that "total" doesn't mean you can run a program in any practical sense:

Fixpoint iterate (op : nat -> nat) base b :=
match b with
| 0 => base
| S b' => op (iterate op base b')
end.

Fixpoint arrow (k a b : nat) :=
match k with
| 0 => a * b
| S k' => iterate (arrow k' a) 1 b
end.

Define grahams_number := iterate (fun n => arrow n 3 3) 4 64.

Sorry for asking questions that may be naive, but do non-terminating type-level functions invariably cause unsoundness of the type system?

(Practically, a program for which the type-level runs into an infinite loop would never be run: since the compiler doesn't return, there's no way to run the executable.)

The Type:Type system first described by Martin Lof is famously non-terminating, however it remains type safe by a general theorem concerning type safety of Pure Type Systems. The situation is similar if you add datatypes and general recursion. However, in addition to loosing decidability of type checking, you also loose the advantages of the Curry-Howard logical view: types can no longer be seen as propositions in a consistent logic.

An example: in a dependent type system with general recursion (e.g. epigram :) we may define the type

OrderedList = {l:List | is_sorted l}

But then ([1,0],proof_of_False) would be a valid inhabitant of this datatype, which as you may suspect seriously diminishes the interest of using dependent types to specify the behavior of our programs.

C's preprocessor, Scheme macros, and C++ templates are all Turing-complete. This isn't as troublesome as you might think. It is more a problem if we don't have any expectations about how long the typecheck, at a given layer or stage, should run.

Our 'gain' exists insofar as we use the stages differently.

I was under the impression that it couldn't encode general recursion. A quick google seems to support this as TM-simulators have used an external tool to close the loop. I'm just curious as this doesn't affect the point that you were making.

I was reporting what I've heard, but digging mostly turns up the external tool to close the loop. So it seems I'm in error on that premise.

2001, IOCCC winner, Best abuse of the C preprocessor

I recall from the way-back-machine that the mini-m4 macro processor in "Software Tools in Pascal" (Kernighan and Pike? - don't recall exactly) supported looping via recursion, so I figured that cpp likely would as well.