search

HigherOrderCO / Kind

A modern proof language
https://higherorderco.com
MIT License
3.58k stars 142 forks source link

Haskell implementation #16

Closed o1lo01ol1o closed 5 years ago

o1lo01ol1o commented 5 years ago

Hi, I started a haskell implementation of the formality language a few months ago but ran out of bandwidth before I was able to complete it. It's here in case anyone want's to pick up the work: https://github.com/o1lo01ol1o/formality-hs

looking forward to an LLVM target for formality-core :)

johnchandlerburnham commented 5 years ago

Neat! I've also been working on a Haskell Interaction net implementation with @cwgoes: https://github.com/cwgoes/formality-experiments

Maybe we can integrate these two efforts...

cwgoes commented 5 years ago

@o1lo01ol1o Cool! Looks like you started on the higher-level part in https://github.com/o1lo01ol1o/formality-hs/blob/master/src/FormalityHs.hs.

Maybe @johnchandlerburnham and I could help with the interaction net runtime.

o1lo01ol1o commented 5 years ago

@johnchandlerburnham @cwgoes
Cool! I think I basically left off needing to write tests against a reference implementation; there are probably a few issues that got transliterated from the JS code. In any case, I'm happy to put it somewhere it can be built on -- I will only have little bits of time to contribute for the near future (though I really am itching to build an LLVM IR compiler for EAC and SIC; not that I have much experience with either . . . ) How ambitious is your effort? Do you want to make a Formality-hs group? Or maybe @moonad would like to host the work?

johnchandlerburnham commented 5 years ago

I think having @moonad host a formality-hs repo would work, but if understand the current plan correctly, Formality is going to be rewritten in Formality-core, so maybe we should start by just adding a haskell directory alongside the javascript in https://github.com/moonad/formality-core ?

@MaiaVictor what do you think makes the most sense?

Also, I've made a Moonad Discord server here: https://discord.gg/WprwbDc

VictorTaelin commented 5 years ago

Oops, I think I missed this issue. Sorry. Please notify me if this happens again.

Please, let me know what you think of the new structure of those projects, as described here. I essentially renamed Formality to EA-TT, since it doesn't include machine ints. This language extended with machine ints and pairs becomes FM-TT (which wasn't implemented yet). FM-TT with syntax sugars is what we will ultimately call "Formality".

I think a healthier/simpler way to port Formality to other languages (Haskell, Rust, Python, whatever) is to implement it in Formality-Core, and then implement its runtime, Formality-Net (a 400-LOC file), in whatever target language we want Formality to be. Otherwise we'd have a code explosion when Formality gets new features. In fact, I think everything I've done should be ported to Formality-Core, it should be the ultimate cross-platform language.

Of course, direct interpreters are welcome too. The file implemented here should probably like at Elementary-Affine-Type-Theory/haskell (on this repository).

Does this make sense?

o1lo01ol1o commented 5 years ago

Makes sense to me. The above lib will take some porting to get to parity with EA-TT (since it was based on an earlier version of the syntax). Feel free to close this.

LoPoHa commented 5 years ago

why would you prefer to implement formality in formality-core rather than formality itself?

VictorTaelin commented 5 years ago

@johnchandlerburnham https://github.com/moonad/formality-haskell seems to be missing, can we create it with my EA-TT.hs implementation?

johnchandlerburnham commented 5 years ago

@MaiaVictor Yes, let's do it