Recently developed software that makes use of refinement types?

[kidq330]

Hi, I think it's safe to mark this issue as [question]

I was wondering if a list of projects utilising liquidhaskell is maintained anywhere, I am really curious about how refinement types play with run-of-the-mill development. The only project I could scrounge up was a cryptographic library that seems to have abandoned LH since experimenting with it a few years back. Projects that are not written in LH but use refinement types are also welcome. I'd be glad to hear from anyone here that is expectedly more versed in the topic whether there is a systematic way to search for these types of endeavours.

On a second note, I've recently come across a seminar on implementing refinement types in typescript, which mentioned the DefinitelyTyped project. This is kind of like Hoogle with the difference that the type signatures need not be provided by whoever is responsible for a function/library, and this typing is instead delegated to the community. Would it make sense to create a similar database where Hoogle functions were more restricted using LH? I can see many considerations going into why this might not be doable, custom types, monads and APIs designed by various libraries, a standard lib of refined types would surely help, but is there some inherent property of refinement types that would make it more difficult? I only recall single opinions that they complicate refactors, but had no luck in finding any article or more involved study that would go deeper into this (a question of refinement systems' maturity?).

I am interested in the LH community's thoughts. Thanks for all the great work!

[nikivazou]

I do not know either and would be very curious on these answers :)

Having a database of libraries verified by LH would be very exciting!

[kidq330]

I found this handy Hackage list https://hackage.haskell.org/packages/reverse but it seems no released packages use it as a dependency :( though I can see people using LH for development only, kind of like DbC

I might hack a script to crawl GH for *.cabal files that contain LH, so I'll leave this ticket open until that happens.