Conversation

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

· Sep 12, 2018

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?

Jacques Carette

@jjcarett2

Sep 12, 2018

Cool. Does it do different sizes of infinities? Some types really are bigger than others...

@edwinb@types.pl

@edwinbrady

Sep 12, 2018

At this stage I'm sticking to 0, 1 and many. But the possibilities are really interesting...

Dominic Orchard

@dorchard

Sep 12, 2018

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).

github.com

GitHub - granule-project/granule: A statically typed linear functional language with graded modal...

A statically typed linear functional language with graded modal types for fine-grained program reasoning - GitHub - granule-project/granule: A statically typed linear functional language with grade...

and I are working on some blog posts about this to advertise what we are doing here (also joint with

Replying to

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… 🤔

9:34 PM · Sep 12, 2018Twitter Web Client

Replying to

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.

Brendan Zabarauskas

@brendanzab

Sep 12, 2018

I guess the issue I'm having when thinking about adapting it for systems programming is that you might want to treat allocation as an effect that you can run on different things, like an arena, ref counting, or GC. Your graded coeffect/effect stuff seems like it could be handy.