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