Closed dougalm closed 1 year ago
I think that you are describing Scala case classes. ;-)
I think that you are describing Scala case classes. ;-)
Yes, that looks pretty close actually. Thanks!
Lean uses namespace for this. For instance, constructor c
of an inductive type T
is automatically put into the namespace T
.
Lean uses namespace for this. For instance, constructor c of an inductive type T is automatically put into the namespace T.
Ooh, that's really slick. I like the open
command.
Is this done now? We don't have def Foo.bar
syntax yet for re-entering a namespace, but as of #1261, I believe the spirit of this idea is fulfilled. Maybe refile the remaining task(s) as (a) separate issue(s)?
Yes, I think this is done for now! My OOP envy has now faded to a very pale green.
Simon Peyton Jones envies OOP and so do I.
Let's say I want to represent a Gaussian parameterized by its mean and variance. I want a type constructor, a data constructor and getters for each field. Here's what I have to do in Dex today:
The boilerplate is annoying but what really bothers me is that I have to come up with four global names:
Gaussian
,MkGaussian
,gaussian_mean
,gaussian_variance
. And then I need to remember those names every time I interact with aGaussian
object. In OOP land, you expect to be able to define the struct like this:and use it like this:
Much better, right?
The constructor name (
Gaussian.new
) comes for free given the type name. We still need names for the fields, but they're now local to theGaussian
type. And since they're local they can be short. We don't care ifmean
andvariance
are already top-level names or if other objects use these names for their fields. When we create the typeGaussian
we get a protected name space for its data and functions. I haven't mentioned functions until now, but OOP lets you bundle functions ("methods") with your object types too. I want that too:I don't care about any of the other OOP stuff -- inheritance, subtyping, factories -- but I really want this, the "power of the dot".
Isn't this just records?
I don't think so. Dex's records don't create a distinct type unless you further wrap the record type with a newtype constructor. So that means (1) you get worse type errors because type inference gets to "look inside" the record structure and (2) you can't add custom instances. Even if we bundled record declaration with creating a new nominal type (like Haskell does), you still wouldn't be able to add type-namespaced OOP-style methods to that type.
Isn't this just type classes?
I don't think so. Yes, type classes do let you overload names, but they encourage you to do it in a very uniform way. If you're writing an instance for
Eq Gaussian
, you don't get to write an arbitrary function for(==)
. It has to be a function of typeGaussian -> Gaussian -> Bool
, and it's expected to be associative, commutative, and satisfy(x == x) = True
. The benefit of that restriction is that it means you can sensibly use(==)
in a polymorphic context. You can write useful functions likehas_duplicates :: Eq a => [a] -> Bool
where the only thing you know abouta
is that it implementsEq a
. But the cost is that everyone needs to agree on what(==)
is supposed to mean.(==)
is still a global name.The dot-style overloading doesn't have any of that uniformity and coordination. Each type just gets its own name space to use however it likes. That does mean you can't use the dot-style overloading in a polymorphic context. Writing
foo.bar
requires afoo
with a concrete type (or at least a concrete head). But there's a benefit to restricting it to concrete types: the rules for resolving the namebar
can be anything we want and they don't have to be expressible as type class resolution.Implementation proposal
Unfortunately the actual dot character
.
is currently used for indexing. I think we should retire it from that role so it can serve this one but that's a separate discussion. For the initial implementation we can use~
or something instead of.
, but I'll keep using.
here for consistency.We'll want to iterate on the specifics but I suggest we start with the following:
<identifier>.<identifier>
toUExpr
. CoreIR/SimpIR doesn't change at all.EMap TyConName SourceMap
registry to the top-level environment that maps type constructor names to the names of the functions and data they refer to.x.y
during type inference as follows. Ifx
is the name of a type constructor, look upy
in the source map associated with that type constructor and use the value directly. Otherwise try the same thing with the type ofx
and then apply the function we find (it has to be a function in this case) tox
. Otherwise throw a type error. There are questions about the order in which we try to resolve types vs field names. We'll probably eventually want to interleave them like we do with dictionary synthesis.def
to use tycon-qualified names, likedef Gaussian.log_density
. Then we can start adding syntactic sugar like thestruct
syntax above. We might even want to go OOP-wild and allow a type and all its methods to be defined in one big block like a Python class.