Struct field access fails if expression type is not yet concrete about numbat HOT 4 CLOSED

Thank you for testing my implementation and reporting this!

This is something I completely missed. It might be a bit harder to fix. It's not related to lists. Here's an even simpler example that also fails:

fn id(x) = x
struct F { x: Scalar }
id(F { x: 1 }).x

The problem is with the polymorphic function call (head or id), because we create a fresh type variable for the instantiation of that function (e.g T0 -> T0 for id). We then add a T0 ~ F constraint matching the parameter type with the argument type, but as you pointed out, that will only get solved after we look up the type for the .x field access (the return type T0 in this case), leading to a "Can not access field 'x' of non struct type 'T0'" error.

My guess is there just needs to be a zonking step performed before looking up the struct type for field accesses?

Hm. Are there general rules for when this is okay? We are currently solving constraints (and then zonking unification variables) only after we have looked at (and elaborated) the whole statement. We are not doing classical Hindley-Milner Algorithm W, where constraints are solved immediately when they are discovered. Instead, I tried to implement a strategy called "constraint typing", where constraints are first collected and only solved after looking at the full statement. I'm not a type theory expert, so I might have made some mistakes. But it is my understanding that this formulation is more suited (or even needed) for Numbat because (1) we need to support dimension types and (2) we want to support type class constraints.

From my understanding of the literature, the constraint typing approach is not strictly needed for (1), but Algorithm W needs some rather complex adaptations to support dimension types directly, while the formulation is more natural using constraint typing. And type class constraints (2), like the Dim constraint that we already have, also nicely fit into this formulation. And I think they can't be integrated into HM directly(?).

Something that doesn't fit well into the current type system are the nominally typed records that you implemented (because I asked you to). Looking back at this, I was recently thinking if structurally typed records would have been the right call after all 🙃. I think they fit better into functional programming languages, and they can fully support type inference (for example: PureScript has a powerful record system using row polymorphism). But nominally type structs still feel a bit more natural to me.

And I thought that we could get away with this by simply requiring type annotations for usage of structs. So something like fn f(x) = x.foo would simply not be supported. I thought this was a reasonable limitation. But this bug shows that I didn't think this through...

Maybe the solution would be an additional constraint? I quickly thought about this when I encountered a similar thing that you reported here... but then I found another solution for that case (whenever we have closed types, i.e. without any unification variables, we now try to pass them from the inside to the outside as far as possible. This didn't just solve my problem with struct field accesses, but also leads to much better error messages. Otherwise, we would only see constraint solver errors, which are horrible). The additional constraint could be something like HasField(expression-type, field-name, field-type). The way this could work looks like this:

When we encounter a field access expr.x, we would not require direct knowledge about the type of expr (and force it to be of the right struct type). Instead, we would only generate a new HasField constraint that we could later solve. We wouldn't know the field-type just yet, so we would generate a fresh type variable, use that in the constraint, and return it as the type of the field-access expression. For the id(...).x example, we would generate the constraints

T0 ~ F
HasField(T0, "x", T1)

and return a type of T1. We would then solve the first constraint with a T0 := F substitution, turning the second constraint into

HasField(F, "x", T1)

Whenever the first argument in the HasField constraint has turned into a concrete type, we can attempt to solve it by looking up whether or not that type (F) has a field with name "x". If it does, we solve that constraint by substituting T1 with the looked-up field type (Scalar in this example).

If someone knows more about type systems then I do, I would really appreciate some help 😄. But right now, I'm thinking this might be a way out for this particular problem.

from numbat.

Oh, haha: https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/hasfield.html

Need to read it in detail, but sounds very much related to the discussion here

from numbat.

HasField constraints are a good solution and I've used them often in haskell. But there's some considerations I can think of:

• If we allow users to use HasField then we will need to support dictionary passing or monomorphisation in order to allow typing:

  fn foo<Y, X: HasField<"y", Y>>(x: X) -> Y = x.y
  

  So that this function is able to access y it can either be passed an extra accessor function at runtime, monomorphised, or we can change the runtime representation of structs to Map<String, Value>.
• However if we don't expose the HasField constraints, then I think it should always be possible to solve the HasField constraint into the concrete struct type.

Rust I think is a good example to look into here, there is no exposed HasField constraint, yet a field access always has to resolve a concrete type.

from numbat.

#461 implements a simple version of HasField constraints.

If we allow users to use HasField then [...]

Right. Since we don't have other types where field access would be useful (except for some of the builtin types like DateTime which are not customizable), I think I would keep that constraint internal for now.

• However if we don't expose the HasField constraints, then I think it should always be possible to solve the HasField constraint into the concrete struct type.

👍

Rust I think is a good example to look into here, there is no exposed HasField constraint, yet a field access always has to resolve a concrete type.

I think this is what we have now with #461 as well.

This discussion here also made me realize that there is a similar problem with one another builtin type (DateTime), that sparks a whole discussion around multi-parameter type classes / traits with associated types, for which I opened a new ticket here: #462

from numbat.