Advice for implementing type aliases

[imalsogreg]

I have forked grace to use as a language for specifying biologically realistic neural networks, and I would like to provide the user with a few (hard-coded) type aliases, like:

• Neuron ~ { segments: List Segment, membranes: List Membrane }
• Membrane ~ List { channel: Channel, channel_conductance: Real }
• Channel ~ { activation: Optional Gating, inactivation: Optional Gating, gates: Natural }
• TimeConstant ~ < Instantaneous | Exponential { tau: Real } | Linear { slope: Real, offset: Real } >

My ideal type aliases have a similar role to Haskell's newtypes: they constrain the type of the value they contain, in addition to just providing a syntactic shorthand. And any value that satisfies the right-hand-side should ideally be inferred to have the type on the left-hand side.

I'm a bit stuck in the design:

• I might add new values to Syntax.Scalar, making a concrete Neuron, Segment, Membrane scalar type, and then have the infer function return these directly if inference encounters the compatible record or alternative.
• Or maybe there should be a new Type called Alias { name :: Text, type_ :: Type s }, and resolving type aliases should be done abstractly.

Do you have thoughts about these? Or is it known that type aliases are just incompatible with grace's bidirectional type checking for some reason?

Thanks! And please feel free to close this issue as off-topic, if it doesn't belong here in Issues.

[Gabriella439]

In general aliases will not work perfectly well because you can't guarantee that they propagate intact to error messages and type errors.

For example, the simplest solution would be to replace the alias with the thing it represents at parse time (e.g. treat it as syntactic sugar) but then you'd never see the alias in inferred types or error messages.

You could try to preserve the alias in the syntax tree (e.g. using Alias) but even in that case the alias might still disappear in certain circumstances. For example if you do something like:

let foo : Neuron = …

in  foo.bar

… that will initiate a subtype check to see if Neuron is a subtype of forall (a : Type) (a : Fields) . { bar : a, b }. In the simple case you could replace Neuron with the equivalent record type at that point in the code or you could update the record-specific subtype check to add special logic for handling Neuron (and possibly an error message specific to the Neuron type)

I guess what I'm trying to say is that it really depends on how much work you want to do. The more you want to preserve those type aliases in inferred types and error messages then the more invasive the change to the codebase.

[imalsogreg]

Thanks @Gabriella439 !

My own priority is:

• Declaring something Neuron with an annotation causes the typechecker to assert the record has at least Neurons fields (or, that it has exactly Neuron's fields, if this is easier).

And everything else is optional. e.g. I don't care much about the type aliases appearing in inferred types, I don't need to be able to use a Neuron as a subtype of larger records, etc.

My users will mostly be copy-pasting code examples and tweaking them. So the aliases are primarily meant to catch spelling errors and accidentally omitted fields.

Given that, maybe the best way forward is to update the record-specific subtype check, adding special logic for Neuron?

[Gabriella439]

Then the simplest approach is to desugar Neuron to the equivalent record at parsing time

[imalsogreg]

Oh yes, this makes a lot of sense. Thank you!!