Hacker News Reader

Comment by slightknack | Hacker News Reader

Any type system with dependent types (`where` in Passerine) is undecidable, meaning error reporting for these types has to be moved to runtime.

There's a quote from someone somewhere, and it goes something like this:

> Ocaml is still trying to develop a macro system that Racket folks won't laugh at... and Racket is still trying to develop a type system that doesn't trip Ocaml fans into a tizzy.

Given that Passerine takes cues from both ML and Scheme, I've kinda given myself the Sisyphean task of bridging this divide. I'm still trying to find the right balance - I did macros first, so I can say I know more about how they work in Passerine - but I hope with a complementary static type system Passerine will become that much more useful.

View on HN

> Any type system with dependent types (`where` in Passerine) is undecidable, meaning error reporting for these types has to be moved to runtime.

Maybe I am misunderstanding you, but this is very confusing. Most dependently-typed languages do in fact check types at compile time: the undecidability problem usually implies a compromise that “correct” programs will be incorrectly rejected (the compiler gives up earlier than it needs to) instead of letting the type-checker get stuck in an infinite loop. But it does not mean type-checking is simply moved to runtime! I am sincerely confused where you got this idea, which makes me wonder if I misunderstood you.

Can you elaborate on the undecidability bit? The task that isn't decidable is, what, "Given a program, determine whether the types are respected in all assignments" ?

I'm pretty sure that the calculus of constructions has dependent types, but wikipedia says that it is strongly normalizing, and I'm pretty sure that determining whether a program is valid in CoC is decidable? (Right? I could be wrong..)

I'm no type theory expert, but if you can describe natural numbers as:

    Even (n: Natural) | n % 2 == 0

Then what's stopping you from doing:

    Undecidable _ | loop {}

I'm not sure, but I think that's because strict dependent language systems like Pie (similar to CoC) use induction over the structure of a type for decidability. If I had 'the little typer' on hand, I'd elaborate more on this point. I think there's some relation between undecidability and the type Absurd, but I'd have to look into it more.

Oh, I think I just confused refinement types with dependent types. The above still stands though.

Just FYI, most dependent type systems don’t typecheck when a parameter to a type constructor is a function, since they can’t “deduce” very much about a function except its signature. They can take proof objects (including objects involving evaluated functions, like ‘n % 2 = 0’) but not functions by themselves (like ‘loop {}’).

This isn’t a technical problem with unification, the issue is a fundamental conflict between “intensional” versus “extensional” equality. Wikipedia has a good example that communicates the underlying confusion: https://en.wikipedia.org/wiki/Extensionality

AFAIK all depedently-typed general-purpose languages use intensional equality since it’s consistent, but there are proof-checkers that use extensional dependent type theories (inconsistency is less of a problem than you might think, and actually makes some higher-order topology and set theory much easier to program).

> I'm pretty sure that the calculus of constructions has dependent types, but wikipedia says that it is strongly normalizing, and I'm pretty sure that determining whether a program is valid in CoC is decidable?

If you write a program in Coq where termination is not trivially true, you need to do the work and write a manual proof of termination. Given a program and something you claim to be a termination proof it's decidable whether that program with that proof is terminating and hence valid in CoC. Given an arbitrary program but no termination proof, I don't see how it can be decidable whether a termination proof of that program exists. You can write a Turing machine simulator in CoC (but won't be able to write a general termination proof).

For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops.

Ok, so the assumption I left out was, “for a turing complete language” or something like that (uh, in a sense in which “takes in a description of a Turing machine, an input to it, and a maximum number of steps, and runs the tm for up to that many steps” doesn’t count as turing complete)

> For some reason I thought CoC just didn’t allow programs that lack a termination proof. Oops.

I'm not sure about CoC-the-abstract-calculus-on-paper, but I guess it cannot allow programs that lack a termination proof. Coq-the-concrete-implementation-of-CoC does allow some. Or not, depending how you look at it: What it will really do is infer a termination proof behind the scenes for certain simple cases, like iterating over a list and the recursive call always being on the tail of the current list. So everything has a termination proof in Coq, it's just that in simple cases you get it for free.

Reply on news.ycombinator.com