Clarity on Extensible Record Type?

[edwardpeters]

Extensible Record Type has some oddities I'd like to better understand:

1. Is the correct interpretation of:

type alias Base = {name : String}
type alias Extension b = {b | number : Int}
type alias Full = Extension Base

That Full is Base extended by Extension (i.e., the record type {name : String, number : Int}, and that in general, when an ExtensibleRecord type is applied to a Record type it creates a Record type equal to the base type extended by the specified fields?

If not, what is a better explanation?

2. If so, can someone explain why the IR wraps a Name rather than an actual Type? It seems like it should be structurally similar to List, Tuple, etc, where it has an "Inner" type (which might be a Variable with a Name), but that generic could have concrete instantiations bound to a particular type. (The documentation also seems unclear on this, as https://package.elm-lang.org/packages/finos/morphir-elm/latest/Morphir-IR-Type#extensibleRecord seems to describe exactly what I'd expect on the RHS of the ==, but all the code I've found only refers to ExtensibleRecord as wrapping a Name...)

3. I'd also like to confirm my understanding that extensible record type does NOT imply that any actual polymorphism exists in Morphir - e.g., you cannot have a list of extensible records which all share a name field but have different other fields. Is that correct?

Finally, I've had some issues exploring the semantics both in elm and morphir-elm (see finos/morphir-elm#1094 ). I want to check if my understanding of the following specific edge cases is correct:

4. If the inner type and the extension share a field name with different types, the extension type overwrites the base - i.e, in the below code someField is an Int in Full

type alias Base = {someField : String}
type alias Extension b = { b | someField: Int}
type alias Full = Extension Base -- Full == {someField : Int}

5. If the inner type is not a record type at all, this is a type error. (I.e., the following is an error:)

type alias Base = Int
type alias Extension b = { b | someField: Int}
type alias Full = Extension Base -- Full == {someField : Int}

(This case is interesting because it means that Extension Record does not fit the pattern of other generics, i.e., being truly generic across any type... this case also behaves oddly in Elm, causing the Ellie compiler to break (it does not compile, but does not report an error), and gives a poorly-formed error in native elm:

The 1st argument to `foo` is not what I expect:

17| test _ = foo {number = 4}
                 ^^^^^^^^^^^^
This argument is a record of type:

    elm: Used toErrorType on a type that is not well-formed
CallStack (from HasCallStack):
  error, called at compiler/src/Type/Type.hs:541:21 in main:Type.Type

For context, I'm working on a design for a type inferencing mechanism in morphir-scala, and most of where that hits stormy waters is around extensible records.

[AttilaMihaly]

Extensible records are a poorly documented feature in Elm so your questions are very valid. Here's what I learned so far:

• They were mainly designed to be used in function signatures rather than stand-alone type aliases for reuse.
• While they do use variables they are not the same as other generic types.
• They are not representing inheritance.
• The closes structure in Scala is a structural type.

Since you mentioned type inference I think it's easier to understand if you look at them from that perspective. Let's say you define this simple function:

foo a =
  a.bar + 1.5

Since type annotations are optional in Elm it needs to be able to infer the type of a here. You might think that the type would be { bar: Float }, but that's not accurate because that would mean that you cannot pass in any value that has more fields even if they do have a bar: Float field. That's because record types require an exact match on the fields of record values.

And that's where extensible records come in. When you say { a | bar : Float } that changes the meaning to: the record value should have at least a bar: Float field. So the inferred types look like this:

foo : { a | bar : Float } -> Float
foo a =
  a.bar + 1.5

To understand why you need the variable name in there, you just need to consider the record update syntax:

foo2 a =
  { a |
      bar = a.bar + 1.5
  }

In this case, we are returning the same type that came in, but the only thing we know about it is that it should have at least a bar: Float field (it can have more). With the type variable we can easily do that:

foo2 :  { a | bar : Float } -> a
foo2 a =
  { a |
      bar = a.bar + 1.5
  }

Without the type variable we wouldn't be able to express the relationship between the input and output types.

I think this is all pretty logical. Things start to fall apart when you are using them in type aliases similar to generic types. As you pointed out the semantics there become blurry. In my opinion Elm should just ban that type of usage as it has no practical applicability and it's very confusing. But even if Elm doesn't we should probably ban it in Morphir. The only reason we haven't done so yet is that people never use it in business models, but banning it explicitly would be a much better approach.

[AttilaMihaly]

For context, I'm working on a design for a type inferencing mechanism in morphir-scala, and most of where that hits stormy waters is around extensible records.

Are you implementing type inference for the Morphir IR in Scala? If so, I think we should coordinate. We do have a type inferencer in Elm and to set expectations it took several months of effort to build it and it involved getting deep into understanding how the Haskell type inference works. It uses an optimized version of Hindley-Milner type inference and it took quite an effort to get it right. Also important to note that it's very different from how the Scala type inference works for example (which is why the Scala compiler often fails to infer the types for the generated code that we already type-checked on the Morphir side).

Given the complexity I think it would worth investigating what effort it would take to port the Elm implementation rather than building one from scratch. Given that it's simple Elm code we might be able to use Morphir itself to do the porting for us.

[DamianReeves]

I think the closest thing on the Scala side is existential types which were dropped in Scala 3.

[AttilaMihaly]

I don't see how they are related. Can you elaborate on why you think they are closer to existential types than structural ones?

[AttilaMihaly]

This is how foo2 would be written in Scala 2 in my opinion:

def foo2[A <: { def bar: Float }](a: A): A

[edwardpeters]

First, I want to (vigorously!) second banning extensible record types in morphir-code (not sure if you mean only banning them there, or also on the back-end, but I'd support either.) The fact that no one uses them currently would argue in favor of banning them sooner rather than later, to me (i.e., before anyone starts.) The inferencer I'm working on really only has trouble with some particular niche cases around inferring extensible record types, and they seem to not fit the pattern of the type system in general. (The fact that one of my examples above breaks elm's compiler makes me think that.)

I'm still unclear why in the typeIR ExtensibleRecords only take a name, rather than an actual type . At least in intermediate states, you might want to resolve that variable to an actual type, and have an ExtensibleRecordType representing that). For instance, if you have

type alias WithBar a = {a | bar : Float}
type alias JustFoo = {foo : String}

And then somewhere in your code you recognize something as being a WithBar JustFoo, you would likely want to bind the a to the value you have in scope (JustFoo), giving you a type {JustFoo | bar : Float}, which you could then recognize was equivalent to {foo : String, bar : Float}. Everything with a name would still work, it would just be {Variable(name) | fields} rather than {name | fields}

[edwardpeters]

So I agree that it behaves differently from proper generic types, especially with unification (part of why I would like to see it banned.) I'm much less clear on the rest, though...

When you say { a | bar : Float } you are not declaring a new type that contains a in any form. You are adding a constraint on type a without introducing any new types.

I am very confused by this. Is that your understanding of how it works in elm? Because in Elm I can absolutely treat this as the introduction of new types... for example, the following is valid in elm:

type alias Base = {name : String}
type alias WithNumber a = {a | number : Int }
type alias Tupled a = (a, {a| number : Int})
type alias Full = WithNumber Base

bar : Base -> Full -> Tupled Base
bar x y = (x, y)

simpleTest () = 
    bar {name = "Blue"} {name = "Red", number = 5}

In that code, if the line type alias Tupled a = (a, {a| number : Int}) were adding a constraint on the type a, then you would expect it to only match tuples of the form (Full, Full) - i.e., both the first and second argument to the tuple must be records with a number field. What am I missing?

As an aside, one minor note is that order actually does matter if the types of fields are over-ridden by the extension:

type alias AInt e = {e | a : Int }
type alias AString e = {e | a : String }
type alias Base = {b : Int}
type alias IntThenString = AString (AInt Base)
type alias StringThenInt  = AInt (AString Base)

foo : IntThenString -> IntThenString
foo x = x

bar : IntThenString -> StringThenInt
bar x = x

In the above code (just in Elm), foo is properly typed but bar is not.

[AttilaMihaly]

The confusion comes from the fact that extensible records work differently in function signatures and in type aliases. The weird behavior comes in in the latter case where you apply the extensible record to a concrete record. You can only do that in a type alias and it's impossible to do when you declare the extensible record as part of a function signature.

And the problem is that when a concrete record is passed in as an argument to an extensible record, for some weird reason Elm decided to "extend" the record structure with additional fields instead of simply enforcing the constraint. I don't understand why it does that because it's clearly different behavior than when the same is done in a function signature:

type alias Foo a = { a | foo : Int }
type alias Bar = Foo {} -- No complaints, it simply adds the missing "foo" field

takeFoo : { a | foo : Int } -> Int
takeFoo a = 
  a.foo

usage =
  takeFoo {} -- Compile error: missing field "foo"

So, I would suggest we ignore the weird case because we'll ban it anyway as it has no practical use.

[AttilaMihaly]

A probable explanation of the weird behavior in type aliases is this: elm/compiler#985

In short, Elm did support adding and removing fields in record types at some point and as the issue points out the mechanism wasn't removed from the type system, only the syntax to do it on values was removed. So it looks like in type aliases it means adding a field while in function signatures it means requiring a field.

[edwardpeters]

Wait, what's different about the function signature? takeFoo doesn't take an a, it takes a { a | foo : Int }... if you code it to take both, it doesn't enforce that a has any fields at all... Unless there's some rule I don't know about that if a variable and a type variable have the same name, the variable is bound to the type of the type variable?

The below code works fine, but would fail if a had to have a foo field:

takeFoo : a -> { a | foo : Int } -> (a, Int)
takeFoo x y = 
  (x, y.foo)

usage = 
    takeFoo {} {foo = 4}

That said, regardless of how it works in Elm, it sounds like the morphir meaning of {<someName> | <someFields>} is "A generic type variable named someName, with the restriction that someName is a record with at minimum the fields in someFields". Is that correct?

[AttilaMihaly]

Yes

[edwardpeters]

Are you implementing type inference for the Morphir IR in Scala?

I've been working on a design for such... I have a particular approach in mind that I've sketched out on paper, but I want to actual code it before over-promising anything (and between it not being a super high priority, and me being out on theoretical limb with the design, that's almost certainly an "In my own time" consideration.) I'll let you know if that process produces any good results.