DEV Community

Discussion on: Feedback request on "hollistic" programming language idea

Collapse
citizen428 profile image
Michael Kohl • Edited on

Personally, I'd probably stay away from forking Idris and removing things, at least for a first prototype. There's a certain amount of joy and freedom that comes with starting from a clean slate and it narrows the solution space less while you're still in the process of exploration:

refinement vs exploration

This may help:

An algorithm for type-checking dependent types

Collapse
drbearhands profile image
DrBearhands Author

That's a good consideration.

A reason for forking Idris 2, other than it having dependent types, is that most of the work I want to do is not based on semantics, but compilation, and Idris 2 already supports multiple backends.

It's something I will have to explore.

Collapse
citizen428 profile image
Michael Kohl

Whichever way you decide to tackle this, I hope you keep on doing it in the open and documenting it here, I for one would certainly love to follow along.

Thread Thread
drbearhands profile image
DrBearhands Author

That's actually really nice to hear, I certainly will!