From a glance it seems to be mostly Haskell-ish but with Scheme style macros.
From the perspective of a very young functional programming language, it is very tricky to balance a powerful type system with powerful macros and I suspect that macros are the priority. The developer also cites the Erlang VM as a major inspiration in terms of a dynamic “expect things to fail and handle it” approach.
Still looks very interesting! I love Scheme (despite having become a static typing curmudgeon) and will be checking out this project.
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.
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..)
Even (n: Natural) | n % 2 == 0
Undecidable _ | 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).
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).
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)
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.
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.