structural types: don't allow multiple constructors of the same type

[ceedubs]

This is relevant to both structural types and structural abilities.

If two constructors have the same type signature then either their name or ordering is going to be important, so the type that contains them really isn't structural in nature.

Consider the following example, where two people have defined a structural logging ability but have put the constructors in the opposite order:

structural ability Log a where
  debug : a -> ()
  error : a -> ()

structural ability Logger a where
  error : a -> ()
  debug : a -> ()

Adding them and using Names Log shows that both Log and Logger do indeed have the same hash:

names Log
 
  Type
  Hash:  #55tq7r3lqg
  Names: Log Logger

We can write a handler that simply shows log messages along with their logging level:

Log.levels! : '{Log a} r -> [(Text, a)]
Log.levels! =
  go acc = cases
    { x } -> acc
    { Log.debug a -> k } ->
      handle !k with go (acc :+ ("debug", a))
    { Log.error a -> k } ->
      handle !k with go (acc :+ ("error", a))
  thunk -> handle !thunk with go []

Since the Log and Logger abilities share the same hash, we can call Log.levels! with either constructor. But the results will vary, because their constructors are swapped.

> Log.levels! do
  Log.debug "debug"
  Log.error "error"
           ⧩
           [("debug", "debug"), ("error", "error")]

> Log.levels! do
  Logger.debug "debug"
  Logger.error "error"
             ⧩
           [("error", "debug"), ("debug", "error")]

Allowing this seems like a footgun. I think that the simplest solution is to make a type/ability fail to compiler if it has two constructors that aren't distinguishable by type.

[atacratic]

Are we sure about this?

It seems like this would also be an argument against passing around tuples like (Integer, Integer), but people do do that.

It has the whiff of a bit of an arbitrary exception to me.

Wouldn't it stop a complex number type being structural? Are we sure we would want to stop that?

[Perhaps an alternative approach would be, when pulling a structural type into the codebase, and finding a match with a pre-existing one, to output a message showing the field names in the metadata on both sides, to give the user a chance to say 'hey those aren't the same!' (Plenty of reasons not to like that approach either though.) Maybe this reconciliation check could also be done at some time later than the pull, when the two types are first actually unified together in some code. That would be quite baroque though.]

To me this seems like a symptom of us not really quite yet being sure what structural types are for and why they are the right solution.

You could imagine (again, possibly baroque) solutions in which there are no structural types, but there are witnesses of type 'equality'/('transportability?') which can be used to transparently give the same kind of behavior, of being able to unify them interchangeably as different bits of code call each other.

[ceedubs]

Are we sure about this?

Nope! Thanks for weighing in.

It seems like this would also be an argument against passing around tuples like (Integer, Integer), but people do do that.

Could you expand upon what you mean by that a bit? (Integer, Integer) showing up in a type signature probably isn't as type-safe as a custom type, but I don't think that it's nearly as problematic as the example I gave above.

Wouldn't it stop a complex number type being structural? Are we sure we would want to stop that?

Hmm that would probably look something like this, right?

unique/structural type ComplexNat = {
  imaginary : Nat,
  real : Nat
}

I actually think that my previous description doesn't cover the case because it's one constructor with two fields as opposed to two separate constructors. But I'm also inclined to think that this is a case that should be prevented.

For example Nat, Nat could represent a complex number, but it could just as easily represent a UUID. You probably don't want to treat that as a structural type, because the structure doesn't define the behavior, and calling functions intended for one will pretty much never make sense for the other. I'm inclined to think that means that it's not a structural type.

To me this seems like a symptom of us not really quite yet being sure what structural types are for and why they are the right solution.

Agreed. And increasingly I'm thinking that it's extremely rare that they are the right solution. The main use-case that I can think of is if two libraries that I depend on use a cons list and I don't want to have to convert long lists of data from one list type to the other if I want to pass objects between the two libraries. Maybe in this case structural types are a technical solution to a community/ecosystem problem, but I do think that cons lists are pretty well defined by their structure.

My instinct is that if the name or order of two fields/constructors matters then the type is not structural.

[atacratic]

Good point that there's a good case for complex numbers not being structural. But it's also sad, because it's exactly the kind of common interchange type where you do want to promote interoperability between libraries that have been written independently. So if we can't handle that case, are structural types really worth it? Or do they just cover a narrow set of cases of very simple parametric types, like cons lists?

I do think they are trying to address a real need (interoperability between libraries written independently). The other ways of addressing it are (a) have a ecosystem-wide canonical libraries (like base) and put as many types in there as possible, (b) write shim layers as and when you need them, (c) implicit conversion stuff (considered a bit of a failed experiment in scala).

Maybe the 'witnesses' idea from the last para of my previous message is the same as (c), I'm not sure.

OK, not sure I have much else to say about the original point this issue was addressing!

Have fun working things out...

[chriskrycho]

An observation: structural vs. unique plays out differently for record types than for custom/union types. My experience with TS and Rust (as well as some Elm and other FP languages) suggests that structural is a good default for record types and nominal/unique a good default for unions—though you still want the opposite around from time to time. (Witness long threads about nominal types in TS and structural unions in Rust!) This is directly related to the distinction between @ceedubs' original motivating example and the ComplexNat example.