Props to them for rethinking the assumptions implicit in the technology! And more props to them for actually being able to comprehend the “Complete And Easy…” paper, which has in my experience been described as neither of those things by most people who’ve read it.
It’s entertaining that the proposed solution is to just special-case a bunch of compiler-defined functions, since that’s exactly how Pascal-family languages handled most things that would otherwise require generics. (And to a lesser extent C-family languages, with things like sizeof().) And of course basically how Go did it for a long time too. So, like, it works, it works pretty well! Sure it kinda sucks sometimes, but it doesn’t prevent you from writing anything you need done. Unfortunately there is a certain type of person, such as myself, who absolutely hates the idea of making built-in functions with interfaces that the compiler is allowed to define but the user is not.
However, a thought occurs to me when they outline the steps necessary for this:
add a bunch of built-in functions…
add special type-checking rules for those built-in functions when they’re fully saturated with all of their arguments…
still require explicit type abstraction when these built-in functions are not fully saturated…
…is there any particular reason you can’t make these rules apply to user-defined functions anyway? I mean, start with a pluggable system that lets people define their own judgements into the type checker, the same way that Haskell’s operator overloading plugs new functions into the parser. Then realize that the type signature of a function is just a shortcut for doing that already? I thiiiiiiiink the cost of this is that type information won’t propagate outside the function, so if you have fnfoo(T) -> T; letx = foo(3i32); lety = x + whatever; then the type checker won’t know that x is actually an i32. At least in some cases. I dunno, I’m bad at this stuff.
(…wait, there’s actually a link at the end describing someone else doing exactly that. Welp!)
The example of if/else blocks is a good case, since in most languages with lambdas and a good optimizer there’s zero reason for if to be a builtin rather than a function, as far as the language cares. The real reason it’s a keyword is not for type checking but because it delays evaluation, and doing that by hand with explicit zero-argument lambdas all the time feels like unnecessary work unless the language makes it really simple. It works just fine though; see Smalltalk, many Forth-y things, etc.
… and if the user were to ask you “How do I define a twice synonym for replicate 2” you would just tell them “Don’t do that. Use replicate 2 directly.”
Yeah, this is entirely practical and very much the cause of the Feels Bad Man™ vibes that make me hate this idea. :-P I would expect this sort of language to very rapidly grow a macro system to paper over these holes, and then you’d spend a lot of your time programming in untyped macros. Kiss the good error messages and coherent semantics goodbye!
I think this “keyword type checking” can potentially occupy a “low tech” point in the type checking design space for functional programming languages that need to have efficient and compact implementations (e.g. for ease of embedding). Also, this can potentially provide a stop-gap solution for novice language implementers that want some sort of a type system but they’re not willing to commit to implementing a unification-based type system.
I thiiiiiiiink the cost of this is that type information won’t propagate outside the function
And ofc that applies to the function. itself, i.e. what will be the type of the variable that you store this function into? It opens a box of lots of issues, which is why I have the same feeling as you: those exceptional built-in things break my intuition about how things work, which is very annoying.
Regarding the foo(T)->T example, I believe the compiler would be able to infer that x is an i32 without unification, whether or not foo was a built-in function or a user-defined function.
In the case of a built-in function, there would be a judgment like:
Γ ⊢ x ⇒ a
──────────────
Γ ⊢ foo(x) ⇒ a
… and in the case of a user-defined function, the foo function would require an explicit type application (e.g. foo<i32>(x)) and that would provide the information necessary to infer the type of the result. Obviously, as the post admits, it’s not ergonomic but it does work (this is basically exactly how Dhall works, and Dhall also does not support unification).
I agree with the rest of what you’re saying, though.
Props to them for rethinking the assumptions implicit in the technology! And more props to them for actually being able to comprehend the “Complete And Easy…” paper, which has in my experience been described as neither of those things by most people who’ve read it.
It’s entertaining that the proposed solution is to just special-case a bunch of compiler-defined functions, since that’s exactly how Pascal-family languages handled most things that would otherwise require generics. (And to a lesser extent C-family languages, with things like
sizeof().) And of course basically how Go did it for a long time too. So, like, it works, it works pretty well! Sure it kinda sucks sometimes, but it doesn’t prevent you from writing anything you need done. Unfortunately there is a certain type of person, such as myself, who absolutely hates the idea of making built-in functions with interfaces that the compiler is allowed to define but the user is not.However, a thought occurs to me when they outline the steps necessary for this:
…is there any particular reason you can’t make these rules apply to user-defined functions anyway? I mean, start with a pluggable system that lets people define their own judgements into the type checker, the same way that Haskell’s operator overloading plugs new functions into the parser. Then realize that the type signature of a function is just a shortcut for doing that already? I thiiiiiiiink the cost of this is that type information won’t propagate outside the function, so if you have
fn foo(T) -> T; let x = foo(3i32); let y = x + whatever;then the type checker won’t know thatxis actually ani32. At least in some cases. I dunno, I’m bad at this stuff.(…wait, there’s actually a link at the end describing someone else doing exactly that. Welp!)
The example of
if/elseblocks is a good case, since in most languages with lambdas and a good optimizer there’s zero reason forifto be a builtin rather than a function, as far as the language cares. The real reason it’s a keyword is not for type checking but because it delays evaluation, and doing that by hand with explicit zero-argument lambdas all the time feels like unnecessary work unless the language makes it really simple. It works just fine though; see Smalltalk, many Forth-y things, etc.Yeah, this is entirely practical and very much the cause of the Feels Bad Man™ vibes that make me hate this idea. :-P I would expect this sort of language to very rapidly grow a macro system to paper over these holes, and then you’d spend a lot of your time programming in untyped macros. Kiss the good error messages and coherent semantics goodbye!
Amen! <3
score 16 · canonical
Yes, I agree with your sentiment. Also:
And ofc that applies to the function. itself, i.e. what will be the type of the variable that you store this function into? It opens a box of lots of issues, which is why I have the same feeling as you: those exceptional built-in things break my intuition about how things work, which is very annoying.
score 2 · canonical
Regarding the
foo(T) -> Texample, I believe the compiler would be able to infer thatxis ani32without unification, whether or notfoowas a built-in function or a user-defined function.In the case of a built-in function, there would be a judgment like:
Γ ⊢ x ⇒ a ────────────── Γ ⊢ foo(x) ⇒ a… and in the case of a user-defined function, the
foofunction would require an explicit type application (e.g.foo<i32>(x)) and that would provide the information necessary to infer the type of the result. Obviously, as the post admits, it’s not ergonomic but it does work (this is basically exactly how Dhall works, and Dhall also does not support unification).I agree with the rest of what you’re saying, though.
score 4 · canonical