Conversation

@edwinb@types.pl
@edwinbrady
That's the one. Incidentally, combining QTT and type driven development is lots of fun. Very handy to have an environment tell you how many of a thing you have available...
Quote Tweet
stephen judkins
@stephenjudkins
·
Replying to @edwinbrady @pigworker and @bentnib
for people who just had a hard time googling it, I assume QTT = "Quantitative Type Theory", from lambda-the-ultimate.org/node/5453?
1
24
Brendan Zabarauskas
@brendanzab
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
Dominic Orchard
@dorchard
Thanks! The challenge is the subtle interaction between dependency and linearity
@pigworker
showed that quantities about usage can resolve this. Definitely interested in quantity-directed compilation, and have some work starting on that soon.
2
4
This Tweet is from a suspended account. Learn more
This Tweet is from a suspended account. Learn more
Brendan Zabarauskas
@brendanzab
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.