3 ms·

An even easier way is to add type parameter to every AST that resolves to either a type or null. It can be relatively easily implemented using type families in

An even easier way is to add type parameter to every AST that resolves to either a type or null. It can be relatively easily implemented using type families in Haskell. And it doesn't suffer the tying the knot shenanigans. The main advantage is that you can still reason about your AST in a straight forward generic manner. In fact this is not only useful for typing. Any kind of metadata that needs to be added can be described in this way. In a compiler I build you had a simple ASTState type parameter for every node in the AST which indicated what is available in the AST. But you could traverse over the entire AST generically as long as you did not depend on any of the additional information. You can basically lift the implementation from this paper: https://www.microsoft.com/en-us/research/uploads/prod/2016/11/trees-that-grow.pdf https://www.microsoft.com/en-us/research/uploads/prod/2016/1...

jez 3y ago
Am I correct in understanding that this means you can only have a list of typed ASTs, or a list of not-yet-typed ASTs, but not a list with a mix? Obviously I understand that if this is the limitation, then there are ways to work around this, and it all depends on how annoying the workarounds are. But I’m curious is there a trick that allows it. All the tricks I can think of involve boxing the the ASTs you’re about to store in the list (which then come with memory/performance hits), and I’d love to be proven wrong.
- jmgrosen 3y ago
  Use an existential type, usually called Some in Haskell: https://hackage.haskell.org/package/some-1.0.5/docs/Data-Some.html https://hackage.haskell.org/package/some-1.0.5/docs/Data-Som... The implementation of this type one has in their head (a GADT) adds a boxing overhead, but the actual implementation in this library uses a newtype. That way if you have a type Expr a, you can have a list type [Some Expr].
- rowanG077 3y ago
  You could make an intermediate step that's only used during type checking which may have partial type information. Then after type checking you lock it down. You can even have HLists but then you are also pretty far along the Ivory tower. I don't think that's worth it.

jez 3y ago

Am I correct in understanding that this means you can only have a list of typed ASTs, or a list of not-yet-typed ASTs, but not a list with a mix? Obviously I understand that if this is the limitation, then there are ways to work around this, and it all depends on how annoying the workarounds are. But I’m curious is there a trick that allows it. All the tricks I can think of involve boxing the the ASTs you’re about to store in the list (which then come with memory/performance hits), and I’d love to be proven wrong.

jmgrosen 3y ago
Use an existential type, usually called Some in Haskell: https://hackage.haskell.org/package/some-1.0.5/docs/Data-Some.html https://hackage.haskell.org/package/some-1.0.5/docs/Data-Som... The implementation of this type one has in their head (a GADT) adds a boxing overhead, but the actual implementation in this library uses a newtype. That way if you have a type Expr a, you can have a list type [Some Expr].
rowanG077 3y ago
You could make an intermediate step that's only used during type checking which may have partial type information. Then after type checking you lock it down. You can even have HLists but then you are also pretty far along the Ivory tower. I don't think that's worth it.