A simple ray tracer in Lean 4

Re:A simple ray tracer in Lean 4 by creata on Monday February 01, 2021 @11:32AM (#25990143)

Are you referring to Linear Haskell[0] or some other effort? Linear Haskell can definitely express destructive updates, but IIRC it needs unsightly stuff like constructors which take continuations and method signatures along the lines of

    length : Array a -o (Array a, Unrestricted Int)

which have to thread the unique value through them, since there's no notion of borrowing.

[0]: https://gitlab.haskell.org/ghc/ghc/-/wikis/linear-types

[ Parent | on HN ]

Re:A simple ray tracer in Lean 4 by ivanbakel on Monday February 01, 2021 @04:02PM (#25993901)

I'm talking about uniqueness typing. It's similar to linear types, but not the same. If you search the term, you can find a few research papers from Dutch universities, particularly around Clean, a programming languages which uses uniqueness typing instead of monads for IO.

[ Parent | on HN ]

Re:A simple ray tracer in Lean 4 by creata on Monday February 01, 2021 @11:52PM (#25997551)

Thanks. I'm aware of that, but I can't find any such efforts for Haskell in particular.

[ Parent | on HN ]