Lambda the Ultimate

For me, bottom would be a value that just means "unknown" - a sort-of wildcard. Divergence would be an observable value. There would be other sorts of expressions in my system that would evaluate to bottom, but simple non-termination would evaluate to divergence, not bottom.

(And thanks for the reference -- I'll check it out)

"Evaluate to bottom" is a tricky concept, because to me evaluation is a computable process expected to return a result in finite time (or never return). Non-termination is mapped to bottom by *denotational* semantics that compile program to mathematical objects (typically morphisms in a category) instead of evaluating them in an operational sense.

It is tricky to find references to Ludics that I find accessible. I've seens a few more approachable uses of Daimon in the work on quantitative realizability (but itself has few easy-access documents, at least until Alois Brunel decides to put his PhD thesis online). I think my best luck in finding a comprehensible presentation of the use of Daimon was in Noam Zeilberger's PhD thesis, Section 4.2.14 "Immediate failure, and the chronicle representation".

My "evaluator" is abstract / denotational. It's a purely mathematical construct rather than something you could implement.

I'll check out that section of the thesis. Thank you.

I don't think this will work for me, but I know I didn't give much context.

The use case is to model types that can explicitly contain divergence. So if Nat is the type of naturals then Nat^_|_ might be the type containing both Naturals and divergence. I don't want this to be the Any type, though.

Even that paragraph probably doesn't give enough context to usefully convey my setup. (I'll have a draft soon if anyone is interested in giving early feedback. I'll give the rules of the logic and a soundness proof. A second article describes how I want to use the system as a foundation for programming language semantics in more details.)

And I've now realized how I should be modeling this. It's pretty obvious really, assuming I'm not making a new mistake. I'm still not convinced it's a good idea, but that will be easier to discuss once I've written it up.

All I need now will be some way to formally reason that divergence yields bottom. I could just add a rule that says that if "f: a -> a" then either "fix f: a" or "fix f = _|_". I'm not positive that's fully general (can be used to establish all cases of divergence), but it seems like it should be. I don't have a special "fix" operator, though, so this doesn't feel particularly elegant.

In domain theory it is usual for domains to contain a _|_ as the least-defined value, and non-divergence, when it is defined through a fixpoint construction (typically to compute the denotational semantics of a recursive definition), usually gets the denotation _|_ among the element of the type's domain (of course there are also forms of productive non-divergence that return partial outputs, and there are other techniques for these, eg. Böhm trees).

I guess you meant that divergence is assigned bottom when it occurs in a fixpoint construction. I do have exposure to domain theory, though I'm certainly not an expert.

Ah, I thought you wanted a value distinct from bottom but part of every type (like null in mainstream languages, if you don't count primitive types). It seems that you want exactly the opposite: a bottom that's NOT part of every type?

I think this is related to effect systems and evaluation order. If an expression e : Nat^_|_, then e either produces a Nat or diverges. But what about a value x : Nat^_|_, can that diverge? (as in a lazy language) Or are values of type Nat^_|_ always Nat? In any case I think the main difficulty is ensuring that an expression e : Nat does not diverge, you need some total fragment in your language for that.

Idris supports both total and possibly not total functions, and the termination checker is aware of which functions terminate and which possibly don't. Though I don't think this is tracked in the type system in Idris. That would indeed be nice.

This page might be relevant: http://adam.chlipala.net/cpdt/html/GeneralRec.html

I'm working on a logic based semantics as an alternative to a calculus with an evaluation order. For example, if you have a parameter with type Nat^_|_, it's not correct to use strict evaluation for that parameter. And if you have a parameter of type (Nat, Nat^_|_), then you could strictly pass the first half of that tuple only.

One of things that I'm thinking is that most dependently typed programming languages force you to be too precise with types in some situations where equational reasoning over expressions would be a better fit. Dependently typed languages don't do a good job of supporting laziness, for example. So that's one thing I'm hoping I can improve upon with this approach I'm writing up (integrating the two approaches).

From very long ago, some hazy recollection: If you can type it, you know it reduces to a normal given the lazy reduction strategy?

Strange if that wouldn't hold for dependent type theories.

Which part of my post are you replying to?

I thought dependent type systems, as in the logical ones, would support laziness pretty well. As far as I know, this was one of the initial reasons why there was so much theoretical interest in lazy languages, guaranteed termination. Some language in which, ultimately, where if you write a well-typed program you know it reduces to a normal/result.

I assume the reduction to normal is probably one of the theoretical bases you need to make a dependent type logic sound, but I am not a type theorist.

But I might have been connecting some dots during the Clean lectures which weren't there.

Well, in dependent languages where every function is total, order of evaluation only affects performance, not correctness. So in that sense, they support it.

What I mean is that if you take a fragment of Haskell and try to give it a precise typing in a dependently typed language that exactly captures the Haskell semantics, that's hard. It would require specifying the conditions under which every parameter needs to have a non-bottom value, for example. But that doesn't mean Haskell expressions are hard to reason about. We can use equational reasoning in the cases we actually care about and never try to assign such an expression a traditional type.

That's not entirely true for coinductive types. Evaluation order has to be lazy for those to terminate (not necessarily the entire language, but constructors for codata have to be lazy in their arguments).

I'm a believer in "post quickly and get things wrong"

Yes, isn't that what discussions are for?

That's not entirely true for coinductive types.

I once talked to a category theorist who tried to explain his arrow marvels, i.e. coinductive types. The great thing about it would be "only deconstructors, no constructors." Where my mind stopped, no deconstructors, no equality, nothing to reason about.

Then I looked at some of the fundamental statements about how it would work. Yeah, nice pictures, some nice theorems about how particular compositions of functions implied injectivity and surjectivity, but no basis in something resembling a formal language.

Just nice pictures and people stating stuff they think holds by an appeal to mathematical esthetics.

I don't think there's anything there, fundamentally. Just some observations which might sometime pan out when formalized, and often will not. Esthetics isn't good enough for formal reasoning.

Do people already try to formally verify Haskell programs? Pending your fragment, that would also imply verifying including type classes and I would assume (since Haskell programmers sometime run into corner cases where they get unexpected results back) that to be hard.

Plus they seem to do a lot of category theory, and I am not sure about the soundness of that stuff.

I remembered why this is probably not a good way to model laziness in a language with precise types. If Nat is a subset of the integers, then a lazy Nat is just a value that's expected to be of type Nat in certain contexts where it will be used. But outside of those contexts, we probably don't want to require that it either be a Nat or divergent. It's perfectly fine if the value is -1 if it's never used.

So this makes me happy that I don't need to go down the rabbit hole of figuring out how to identify divergent computations from within the logic. That seems really ugly.

But here's the dilemma. Let's consider this snippet:

bar: lazy Int -> Bool

foo: lazy Nat -> Bool
foo x = bar x

What should the logic of function foo be here? It doesn't ever directly demand that x be a Natural and only passes x on to bar, which only requires its parameter be an Int. So is x allowed to be a negative number when it's "passing through" foo? Surely not.

The best way I can see to encode the logic of the situation is this:

foo x = let x'=x if x:Nat in bar x'

Here we have a conditional let (which can easily be modeled in terms of logical primitives) that tells us that if x is a Natural then x' is an alias for x and otherwise we know nothing about x'. That means that if the 'in' clause needs to rely on the value of x in any way for its semantics, then x needs to be Nat.

This encoding looks like it might be what I want, but it encodes laziness only on a parameter-by-parameter basis. I was kind of hoping for an encoding that let me have e.g. a list of lazy Nats. Maybe there's some reason why that wouldn't actually make sense? I guess I could try to find a more elaborate encoding of the pattern I've described here. I know that laziness doesn't just change the denotation of a type as a set of values.

Any thoughts? (I know my setup is a little unusual.)

Why would you not require that a lazy Nat is actually a Nat or divergence? We also require a function of type T -> Q to always return Q, not just return Q in those contexts where it's used. A lazy Nat is just a function of type unit -> Nat. To me the whole point of types is that they are valid in any context. That's what enables modular reasoning. If you want to have something that's only a Nat in a specific context then you have to be explicit about it in the type. With dependent types: T = (if p then Nat else Int). Now you can use values of type T as Nat in contexts where p is true.

Doing that automatically for general contexts seems undecidable: you don't know if a lazy Nat will be evaluated eventually or not. For example let n : lazy Nat = delay -3 in if test_goldbach_conjecture k then force n else 4. Or maybe you have a restricted notion of context in mind?

When types don't depend on values, the two concepts are the same: the value context won't change the types and thus if the types work at the use site then they work everywhere. So I think either approach would be a valid generalization for what laziness means with dependent types. But I kind of think my choice is the more practical one. A major requirement is to make it where precise types and theorem proving are optional. Consider this function:

foo p:Bool ~x:Nat = if p then (bar x) else 0

(Note the makeshift notation: tilde marks laziness.) If we take your approach, then the type signature I've provided here implies callers must come up with a valid Nat whether or not p holds. That seems like it will be annoying. On the other hand, I definitely don't want to force the programmer to write down the type that you did in this situation.

We also require a function of type T -> Q to always return Q, not just return Q in those contexts where it's used

Are you sure we do? With partiality as with laziness, I think we should err on the side of convenience. Now, I do have a concept that I'm calling type categories (but am open to suggestions - the mechanism isn't exactly refinement types) that are fully inferrable coarse types like what you'd expect to have in Haskell. Those would behave more context insensitively. [So I'm not going to let you call (foo false 'bob') in the example above.]

The problem is that you've now made type checking non modular. The fact that x only needs to be a Nat if p is true is not reflected in the type. So to type check an invocation of foo you need to look at the definition of foo, not just the type of foo.

Consider something like this:

foo : Int -> Ratio
foo n = 1000 / n 

Do you want to make that a type error because division requires that the denominator not be zero? Or give a less precise type to division? Or require a cast (which throws away the information that n shouldn't be zero)?

The option I like is to not have the compiler complain because it's a partial function annotation. Anyone interested in proving correctness of uses of a partial function or a function with lazy parameters will need to reason about the source non-modularly to do so. Ideally, n /= 0 should be a goal for the theorem prover and I won't see a warning unless it wasn't able to discharge that obligation at the call site. Even then I just want a warning.

This approach allows me to opt-in to the crazy world of dependent types by providing a total function annotation without lazy parameters.

Finally, as I was trying to argue above, I think there are lots of cases where the expression defining the function is easier to reason about than its type. What sense does it make to introduce a complicated type for such a function in the name of modularity when you could just export the function body?