Idris 0.9.15 released – partial evaluation and uniqueness types

Re:Idris 0.9.15 released – partial evaluation and uniqueness... by carloscm on Monday October 27, 2014 @09:01AM (#8515176)

This reminded me of ATS - http://www.ats-lang.org/ Check also Chris Double blog - http://bluishcoder.co.nz/tags/ats/

ATS combines ML-style types, linear types, dependent types and theorem-proving. Plus it compiles down to C, has pointers including (safe!) pointer arithmetic, has trivial C interop, and doesn't have GC (alloc/free safety is provided by the linear types, like with Rust lifetimes). It's a really interesting beast and I hope I have more time in the future to dive into it. Idris wins in the syntax department tho.

[ Parent | on HN ]

Re:Idris 0.9.15 released – partial evaluation and uniqueness... by bjz_ on Monday October 27, 2014 @10:13AM (#8515510)

> alloc/free safety is provided by the linear types, like with Rust lifetimes

Rust's move/ownership semantics are based on linear types, where as its lifetimes are based on regions. ATS has linear types, but not regions.

[ Parent | on HN ]