Hi Chris, this is great! My thoughts on your post below.
My thinking with structural types is that, between different types, the structure of the set of constructors is unique; and within a single type, the structure of individual constructors is unique. Specifically, I very much don't want the declared order of the constructors to matter for a type like Optional. And if the declared order of constructors doesn't matter, then how would you distinguish two nullary constructors, apart from by their (original) names.
Maybe Color / warm / Direction / longitudinal are a bad example / have a mistake in them because, looking at them, I can't see how warm and longitudinal are the same. And I exactly do want to the typechecker to notify me when I'm about to call a function on a value that it wasn't meant to understand.
I'd like to avoid this simply because I think it means that a definition that typechecks in one codebase wouldn't check in another codebase that lacks the additional mapping. I think types that are interchangeable need to have the same hash from the outset.
I was thinking it would be the hash of their initial names, which we do currently retain as part of the type decl's representation. So constructors could still have their own local names, but my thinking with nominal types is that the original names are linked to a specific meaning that doesn't change over time. Renames can be tolerated, provided that they are not so drastic as to change the underlying concept. If we want to update the underlying concept of a constructor in a nominal type, it's time to replace the type altogether.
I agree it feels fragile. I just need a good story for these lists of things for which the names do matter because that's the only structure to them. The names you to reference them can change, but the underlying concept doesn't.
This idea is like defining a type alias but for which only a certain, specified, privileged set of code (not just their signatures) gets to view the two equated types as the same; external code would only be able to use those accessors. Example might be a sorted list with its own definitions for insert, fromList (sort), toList (a no-op), filter (delegates to the underlying list), merge, and that's it. You can write your own code that uses these, but you can't directly access the list it encapsulates.
This one was the least baked, with no plans for how it would be implemented yet. :|
Not convinced I know what you mean by being part of the code, but the nominal/structural distinction would be a directive about how the code is (and was) added to the codebase. It's selecting a scheme for determining which types should be identical, both in storage and from the perspective of the typechecker. Once the scheme is selected and the type is added to the codebase, then we're just comparing hashes.
- Do we want a type's identity to change when we add a new constructor to it? Yes
- Do we want that edit to open up all the definitions that reference that type? In short, yes. We have the concept of a type-preserving term edit, for which changes can be propagated automatically if desired; you could imagine an equivalent automation for certain kinds of type changes.
- Do we want an exhaustiveness checker for pattern matches? Yes
- Can we migrate code ...? Yes, just like any other change, right?
Yeah I think the signatures won't be enough to distinguish types. It's not obvious to me that NumberPrefixMap wouldn't have a size operation, or that RoseTree wouldn't have a lookup operation, right?
I do like the idea of being able to generalize all of these down to a single model if practical.