Hacker News new | past | comments | ask | show | jobs | submit login

If I am not mistaken Agda is similar in this regard too. My question would be how is no garbage collection possible, or how practical is it to use an FP language without GC? I assume I can't get very far with writing ML-like programs without GC.

edit: nvm, just saw that it uses linear (or affine?) types

We use affine types, which means every value can get used at most once. This is a lot less painful in practice than it sounds though, since:

a. we can copy things for free at compile-time that get erased at runtime

b. we have a `cpy` primitive that allows for free copying of our Word type (a 32-bit unsigned int)

c. we have a primitive that allows for deep-copying, as long as the copies (and anything that uses them) are marked with usage annotations https://docs.formality-lang.org/en/latest/language/4.Core-Fe...

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact