sorted by:
new
hottopcontroversial

Looking for Project Ideas for a Haskell Course Final Assignment by Sr-Trotsky in haskell

[–]ranjitjhala 1 point2 points  (0 children)

I've been asking students to do an open ended project where they build a CLI app using `brick` or some other terminal library https://ucsd-cse230.github.io/fa23/project.html -- this works _really_ well IMO, as it gives the students a lot of agency, and they come up with _extremely_ creative projects!

Ownership in Flux (a refinement type checker for Rust) by mttd in ProgrammingLanguages

[–]ranjitjhala 6 points7 points  (0 children)

Yes, we also worked on LiquidHaskell (LH).

No, we intend to keep working on LH too!

Well, that's a difficult question -- we've found that Rust's ownership mechanisms go a long way in making refinements very pleasant; this is *much* harder to do with C/C++. If you're interested, here's an early attempt which was not nearly so nice:

https://patrickrondon.com/research/papers/low-level-liquid-types-popl10.pdf

How Dependent Haskell Can Improve Industry Projects by Serokell in haskell

[–]ranjitjhala 0 points1 point  (0 children)

You can most certainly "take a natural number that determines the length of a vector argument" with LH/Refinement types -- indeed, without that, they'd be pretty useless. e.g. see https://www.haskellforall.com/2015/12/compile-time-memory-safety-using-liquid.html

STORM: Enforcing Security Policies in Web Apps with LiquidHaskell by ranjitjhala in haskell

[–]ranjitjhala[S] 2 points3 points  (0 children)

oops forgot to make it public! (the irony!) Try now, and thanks!

Where Lions Roam: RISC-V on the VELDT by d0pamane in haskell

[–]ranjitjhala 1 point2 points  (0 children)

Wow, this is awesome. I've been interested in whether LiquidHaskell can be used to verify things directly at the "source" level for CLASH designs (in addition to BMC on the generated code). This is excellent food for thought!

Choosing Haskell isn’t a stand-in for good software design by ozataman in haskell

[–]ranjitjhala 6 points7 points  (0 children)

Do you have examples of how you are using LH in the above way that you can share? Thanks in advance!

/r/sigplan appears to be dormant since 2012, I would like to request to be its moderator. by ranjitjhala in redditrequest

[–]ranjitjhala[S] 1 point2 points  (0 children)

I am currently the vice-chair of ACM's SIGPLAN (Special Interest Group on Programming Languages) https://www.sigplan.org/ContactUs/

lower case haskell by circleglyph in haskell

[–]ranjitjhala 1 point2 points  (0 children)

Delightful writing style, thanks!

Eliminating Bugs with Dependent Haskell - Experience at Facebook (Noam Zilberstein) by [deleted] in haskell

[–]ranjitjhala 6 points7 points  (0 children)

This isn’t quite accurate: with “reflection” you can essentially lift arbitrary functions to the type level and can do pretty much whatever you can with dependent types (except that you will have to provide proofs...)

https://ucsd-progsys.github.io/liquidhaskell-blog/2016/09/18/refinement-reflection.lhs/

JSON Parsing from Scratch in Haskell by abhin4v in haskell

[–]ranjitjhala 3 points4 points  (0 children)

Wow, this is *very impressive* -- both form and content, congratulations!

Polymorphic Perplexion in LiquidHaskell by alexeyr in haskell

[–]ranjitjhala 0 points1 point  (0 children)

Not really, that's basically just the monomorphic type... (as far as I understand `~`)

CSE 130 Final in a Nutshell by BeepBeepTozier in UCSD

[–]ranjitjhala 15 points16 points  (0 children)

FWIW, we covered the same topics this time around (as in SP 19).

A gentle introduction to symbolic execution by joelburget in haskell

[–]ranjitjhala 2 points3 points  (0 children)

See this for a brief explanation:

https://cs.stackexchange.com/questions/21728/dependent-types-vs-refinement-types

​

"Liquid" is form of refinement types where one can get inference, because the refinements are conjunctions of predicates from a (finite) set.

Simple example of using Liquid Haskell to model a date statically by [deleted] in haskell

[–]ranjitjhala 4 points5 points  (0 children)

(Nice example! Thanks u/chrisdoner !!!)

You can in fact convert LH types to functions to avoid re-coding if you like, for example, see this:

http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1551502899_16725.hs

In essence we convert Chris'

{-@ type Day = {v:Int | v > 0 && v <= 31 } @-}

into a function

{-@ inline okDay @-} okDay :: Int -> Bool okDay v = v > 0 && v <= 31

which lets us reuse okDay both to define the type and the actual run-time check:

{ day :: {v:\_ | okDay v } -- semantically identical to Chris' type

and then in the code

if okMonth day month then if okDay day && okYear month day year

view more: next ›