Different type IDs can point at the same type

[kubouch]

As pointed out in #50, typecheck_match() looks only at type IDs without actually checking the underlying type. This means that two identical types, such as:

let x: oneof<list<int>, list<string>> = []
let y: oneof<list<int>, list<string>> = []

would have different IDs and result in type mismatch.

Two possible solutions:

1. Change typecheck_match() to actually check the types properly
2. When creating a type, first check whether it's been created already and reuse its ID if so. This would ensure that different type IDs would point at different types.

[ysthakur]

For option 1, perhaps we could store oneof types in a canonical-ish form. I'm thinking if the user types something like this,

let x: oneof<list<int>, list<string>, oneof<int, float>> = ...

the type of x is internally created as oneof<list<oneof<int, string>>, number>. Storing it that way might make comparing types easier. But it might also confuse users who expect to see the original type they annotated xwith.

Option 2 seems like it might cause performance issues because you have to go over the whole vector of types each time you add a new one. Unless we keep the types sorted according to some ordering, or store the types in a special data structure that lets us search easily. Not sure how easy that would be.

[132ikl]

Option 2 shouldn't be bad if we can make type IDs hashable

[ysthakur]

Do you mean making Type hashable? I guess that could work well if we have a canonical way to represent every type. Might get complicated when we add type aliases, though. We could completely expand every type alias to get its canonical representation, but then (similar to the case in my previous comment), users would see that expanded type in error messages/LSP hints, rather than the original type alias.

[kubouch]

Option 1 is cheap to add, but expensive to check. Option 2 is expensive to add, but cheap to check. I think Option 2 is more expensive overall with a large type vector. On the other hand, type checking is probably done more often than type adding, so it might add up.

I like the type hashing though, that would solve the problem. I think it should be possible to work around the error messages with type aliases.

[ysthakur]

I think it should be possible to work around the error messages with type aliases.

Are you thinking about something like what OCaml does, where (afaik) it looks at type aliases in scope and automatically uses those type aliases in error messages?

Option 2 is expensive to add, but cheap to check

I do want to note, we'll also have to check if types are subtypes of other types, not just whether they equal other types, which will be expensive for both options (though a bit less expensive for Option 2). I'm not sure if, in practice, most checked types will end up being equal to each other, though. It's worth benchmarking both approaches.

[kubouch]

Are you thinking about something like what OCaml does, where (afaik) it looks at type aliases in scope and automatically uses those type aliases in error messages?

I haven't thought about that yet, but something like that could work. Or just keep the NodeId around so that the error message can check if it's a type alias.

I do want to note, we'll also have to check if types are subtypes of other types, not just whether they equal other types, which will be expensive for both options (though a bit less expensive for Option 2). I'm not sure if, in practice, most checked types will end up being equal to each other, though. It's worth benchmarking both approaches.

True, we still need to check subtypes.

Forgot to reply to this:

But it might also confuse users who expect to see the original type they annotated x with.

Yeah, seems to me too confusing as well. But again, the error message could just look up the span of the type declaration node and use that, not a big deal IMO. Btw, oneof<list<int>, list<string>> does not equal list<oneof<int, string>>. But I agree oneof<float, int> should be a number, that could perhaps be even a compile error.

[sholderbach]

Subtyping to some extent represents, a less than or equal comparison, I am wondering if we could express that in the cache structure or even the hash.

[ysthakur]

Perhaps a directed acyclic graph of types (to represent subtypes), together with a hashmap mapping type IDs to nodes in the graph?

---

Btw, oneof<list<int>, list<string>> does not equal list<oneof<int, string>>

Whoops, missed that!

[cosineblast]

I apologize for the bikeshedding, but I fear that as our type system becomes more complex, it will become ever so harder to use integer-based heuristics to check for type matching¹. If our time constraints allow for it, maybe checking the types everytime is something to consider

[¹]: If we add generics/parametric polymorphism, type match checking will become at least as computationally difficult as pattern matching/unification

[Bahex]

Is there separation between SyntaxShape and Type like the current parser?
I'm asking specifically because of oneof, as the order of its variants affect how values are parsed in the current parser and may result in different types when the type of a literal is ambiguous.

def closure_record [p: oneof<closure, record>]: { $p | describe }
def record_closure [p: oneof<record, closure>]: { $p | describe }

closure_record {}
# => closure

record_closure {}
# => record

closure_record {"foo": "bar"}
# => record

record_closure {|| }
# => closure

If there is no distinction between syntax shape and type, either oneof's behavior will need to change and order of its variants will be normalized according to some total ordering, or the type checking will be more complicated than needed.

[ysthakur]

@Bahex The new parser isn't type-directed, so there's no longer a concept of syntax shape at all. Parsing happens first (with no regard for types), and then typechecking. I guess the behavior of oneof will be different in the new parser, but parsing ambiguous structures in general will change, so I don't think you need to worry.