Annotate functions with 'LiquidHaskell'

serokell / universum

:milky_way: Prelude written in @Serokell

MIT License

176 stars 28 forks source link

Annotate functions with 'LiquidHaskell' #113

Closed chshersh closed 6 years ago

chshersh commented 6 years ago

LiquidHaskell is a great tool! Before trying it on big projects, we should enhance our infrastructure libraries. Custom prelude universum is a great target for being annotated with LiquidHaskell. Also, once base is annotated, we can reuse specs from base in our functions!

So the plan is:

[x] Read some LiquidHaskell tutorials
[x] Try to launch liquidhaskell following instructions for cardano-sl
[x] Come up with the list of some properties for universum (this list should at least contain Min property)
[x] Impelement those property
[x] Think about how to prove functions totality and which functions can be proven

gromakovsky commented 6 years ago

Also, once base is annotated

Do we know it will happen relatively soon? Just curious and lazy to google :)

chshersh commented 6 years ago

@gromakovsky These annotations are already written during last year Haskell Summer of Code

https://summer.haskell.org/news/2017-09-15-final-results.html

The work can be found here:

https://github.com/sdleffler/ghc/tree/ghc-8.0

I contacted mentor of this HSOC project. Maybe she can share plans regarding merging this work into base package eventually.

chshersh commented 6 years ago

@nikivazou Answered me the following:

Hi Dmitry, I am indeed the best person to reach as I was co mentoring this project. Sadly, it didn't go very well and until the end, there was nothing ready to merge... If you have time to play with it, feel free to merge it:)

So, probably, seems like there's not a single person at the moment who is actively working on LiquidHaskell annotations for base package and we probably shouldn't count on that :disappointed:

chshersh commented 6 years ago

This is partially done in PR #156. More properties can be suggested and added under different issues.