I don’t think this approach requires introducing new keywords for all these operations. You could instead add an infer keyword for type parameters that can always be inferred from the types of the function arguments. So map would change from:

map : ∀(a b : Type) → (a → b) → List a → List b

into:

map : ∀(infer a : Type, infer b : Type) → (a → b) → List a → List b

When calling map, you omit the types a and b and they’re instead inferred from the type of the first argument (a →b).

This gives a more reasonable set of limitations:

• It doesn’t play well with automatic currying, since a curried argument might be required to infer some type parameters. (So the map type signature above is a little misleading, it shouldn’t have nested arrows.)
• You can only infer type parameters that are fully determined by the function arguments. Putting infer on a type parameter that cannot be so inferred would give a type error on the function definition. Instead you would omit the infer, and the caller will have to specify the type parameters explicity. But these are more complex functions so it’s more reasonable to require annotations on them.

score 8 · canonical

What I’m wondering here, is how many rules would go away if instead of giving up on unification altogether, we stuck to local type inference? That would eliminate fewer rules for sure, but how few exactly?

There’s also the question of where the bloat comes from exactly: is it from unification alone, or is it from how unification interacts with everything else? If it’s the latter, then keeping “everything else” small could very well help us keeping a small type system. Personally I wouldn’t ask for much: basic built-in types, sum & product types, a built in array if singly linked lists aren’t enough… and not much else to be honest. Type classes maybe, existential quantification perhaps, and I’d skip inheritance for sure.

score 4 · canonical

For what it’s worth, unification should not be difficult to implement; a bare-bones unification monad without backtracking should take fewer than 100 lines of Haskell, using the µKanren recipe. The type-checker can then be written as type judgements, taking one or two lines for each production. I say this because I don’t like to think of folks having to maintain thousands of lines of excess compiler infrastructure.

For example, consider that Haskell is terser than RPython. In my implementation of Cammy, it takes 148 lines to implement the µKanren core (sampler/cammylib/types.py) and about another 126 lines to type-check 39 productions (sampler/cammylib/arrows.py), without macros. Haskell is also terser than Scheme. The module implementing relational type-checking (allowing type-driven program synthesis) is 289 lines (movelist/cammyo.scm), of which 133 lines are type-checking and the rest are evaluation.

score 10 · canonical

This is a lot of extra steps for just writing code in System F, or one of its numerous variants, aka GHC’s Core. System F is only type checked, there’s no inference. You don’t need to play complex games with having keywords or anything like that. Exactly what you need to annotate is well defined.

score 2 · canonical

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 fn foo(T) -> T; let x = foo(3i32); let y = 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.

Amen! <3

score 16 · canonical