Creating Data Types

[Gaelan]

I see that there are data types available when writing code, but is there support for creating our own yet? If so, I can't figure out how.

[yairchu]

Not yet..

[yairchu]

What's been holding us a bit on this is that we'd like to first change the (Haskell) type for (Lamdu) types to have an external fix-point so it could be stored in the DB each AST node separately like the values are.. But checking how it would affect the type inference performance with our current implementation seemed to slow it down significantly, and Eyal started to write a new faster type inference implementation (https://github.com/Peaker/AlgoWMutable) which is going to be much faster and will support such editing.. However this implementation is not done yet.
This is certainly one of the critical things we need to make Lamdu useful :)

[ysangkok]

What happened with AlgoWMutable?

[Peaker]

@ysangkok It's functionally complete, but its integration into Lamdu was postponed repeatedly for lower hanging fruits till now.

Currently I estimate we'll be able to integrate it within ~3-4 months from now,

[ysangkok]

So sounds like this issue is solved, according to https://gitter.im/lamdu/lamdu?at=5a79e42f36de78850cfbcfb3 ?

[Peaker]

Structural types are mostly usable.
Nominal types are still missing, so our approximation of RankNTypes is not usable directly, and recursive types cannot be declared.

Nominal type editing is one of the next steps, perhaps after integrating AlgoWMutable

[joonazan]

Do you currently rerun type inference every time something is changed? I have been working on a thing very similar to Lamdu so I have tried to find alternatives to that.

The paper Compositional Type Checking for Hindley-Milner Type Systems with Ad-hoc Polymorphism describes a way to infer types so that a subexpression's parents do not affect its type. It would limit the amount of recomputation necessary for a change.

However, it only deals with variables coming from lambdas. Let still builds an environment as usually.

I have implemented some of it but haven't gotten to let and my only ideas for making let compositional would perform very badly.

[Peaker]

Nominal type editing is one of the next steps, perhaps after integrating AlgoWMutable

First, I'll update that we eventually decided to go a different route than AlgoWMutable, and use hypertypes. A smarter more efficient algorithm with better complexity, though currently with a not-as-good a constant (this should be fixable with some tuning).

Hypertypes allow far more flexibility w.r.t representing hetero-ASTs (e.g: a Value-Term AST, that nests Type-AST within it) with flexible fix-points. This is a major milestone for type editing, and we now store editable types in our database.

We're still lacking Codec(JSON import/export) support for it, and of course the sugaring/UI work on top, but that's growing nearer.

Do you currently rerun type inference every time something is changed?

Only for the current definition, in principle. Other definitions have cached/saved exported types.

We have a known issue with this approach, w.r.t co-recursive definitions, but we're not fully happy with the solutions we currently have for it. Primarily, the solutions all require O(N) work upon edits, where N is the project size, in the worst-case. Currently we try to keep all work to O(1) or roughly the amount of code that fits on your screen.