7 ms·

From a glance it seems to be mostly Haskell-ish but with Scheme style macros.

ojnabieoot 6y ago
Hmm, at a somewhat longer glance, I would say it’s very Scheme-ish in its semantics but only superficially like Haskell (and really more like ML generically). Specifically, despite algebraic type definitions, Passerine is dynamically-typed with an emphasis on structural/“duck” typing. The author plans to add a Hindley-Milner type checker but the language does not seem to be “type-centric” in the way I think of Haskell - types will be added for verification, but not as a near-first-class programming construct. I get the impression it might be more like mypy and that runtime type errors will still be a thing. 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.
- slightknack 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. 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).
  - 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.

Hmm, at a somewhat longer glance, I would say it’s very Scheme-ish in its semantics but only superficially like Haskell (and really more like ML generically). Specifically, despite algebraic type definitions, Passerine is dynamically-typed with an emphasis on structural/“duck” typing. The author plans to add a Hindley-Milner type checker but the language does not seem to be “type-centric” in the way I think of Haskell - types will be added for verification, but not as a near-first-class programming construct. I get the impression it might be more like mypy and that runtime type errors will still be a thing. 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.

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