10 Feb
2016
10 Feb
'16
1:02 p.m.
On Sun, Feb 7, 2016 at 10:39 AM, Tom Ellis < tom-lists-haskell-cafe-2013@jaguarpaw.co.uk> wrote:
If we were inventing a language from the beginning, would it be strictly necessary to have two kinds?
Could we have just an unboxed kind #, and have a box be an explicit type constructor?
Does this thing seem remotely plausible to people who know clever type theory?
Idris tries to do this with their Lazy type -- to somewhat mixed success, so yes, it is a thing that can be done in a language designed from scratch.