Cool. Does it do different sizes of infinities? Some types really are bigger than others...
Conversation
At this stage I'm sticking to 0, 1 and many. But the possibilities are really interesting...
2
1
People interested in such things might also like to check out the Granule language github.com/granule-projec which is a linear language with indexed and graded modal types (quantities like in QTT, but not fully dependency... yet).
1
2
7
and I are working on some blog posts about this to advertise what we are doing here (also joint with ).
3
5
Really enjoying the Granule stuff. What are the challenges involved in getting this kind of thing to work with dependent types? I'm also wondering about systems programming questions, like allowing you to customise the dynamic allocator for 'inf' multiplicities… 🤔
1
2
Thanks! The challenge is the subtle interaction between dependency and linearity showed that quantities about usage can resolve this. Definitely interested in quantity-directed compilation, and have some work starting on that soon.
2
4
Also, tracking the quantities throughout the entire system correctly is challenging when considering both term level and type level.
1
4
This Tweet is from a suspended account. Learn more
Are you speaking about this example specifically, or in general? Just been playing around with trying to implement your universe shifting stuff from pigworker.wordpress.com/2015/01/09/uni - was calling the numbers 'levels'.
1
1
This Tweet is from a suspended account. Learn more
Right, definitely have appreciated your work in splitting apart those notions in my mind (especially with regards to your worldly types presentation that you did a while back). Those were definitely conflated for a while in my head.