3 ms·

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

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.

drdeca 6y ago
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..)
- slightknack 6y ago
  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.
  - slightknack 6y ago
    Oh, I think I just confused refinement types with dependent types. The above still stands though.
  - ojnabieoot 6y ago
    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 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).
- tom_mellior 6y ago
  > 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).
  - drdeca 6y ago
    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)
    - tom_mellior 6y ago
      > 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.
ojnabieoot 6y ago
> 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.

drdeca 6y ago

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

slightknack 6y ago
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.
- slightknack 6y ago
  Oh, I think I just confused refinement types with dependent types. The above still stands though.
- ojnabieoot 6y ago
  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 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).
tom_mellior 6y ago
> 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).
- drdeca 6y ago
  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)
  - tom_mellior 6y ago
    > 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.

ojnabieoot 6y ago

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