Conversation

Really want to have dependently typed languages that can combine the two! If anyone has any pointers to ways of combining simple refinements (eg. integers/array bounds) with intensional type theories, I'd love to know, as I'll be needing it for a DSL project I am working on!

Quote Tweet

Talia Ringer

@TaliaRinger

· Jun 11, 2021

I don't think there's a reasonable argument against refinement types being a kind of dependent type. Arguments against this usually just come down to implementation details and people not wanting to associate themselves with us nerdy DTT people

Show this thread

Brendan Zabarauskas

@brendanzab

Jun 12, 2021

I was thinking of adding some kind of 'SMT' universe (or a modality perhaps?) to my language, but I dunno! It doesn't need to be very fancy for this project, I just want to be able to automate away a bunch of stuff to make things easier for users.

Brendan Zabarauskas

@brendanzab

Jun 12, 2021

I was going to look at

@RanjitJhala

and

@nikivazou

's Refinement Types: A Tutorial and sprite-lang, but I think I'd then need to figure out how to combine it with DTT and semantic typechecking/NbE 🤔 • arxiv.org/abs/2010.07763 • github.com/ranjitjhala/sp

Brendan Zabarauskas

@brendanzab

Woops, I just realised I wrote ‘intensional type theory’ when I meant ’intuitionistic type theory’ in the original tweet, but I'm not sure how much it really matters… 😅

8:23 AM · Jun 12, 2021Twitter Web App

Replying to

Choosing intensional type theory matters if having decidable typechecking matters.

Brendan Zabarauskas

@brendanzab

Jun 12, 2021

Yeah, to be more precise I’m interested in intensional+intuitionistic type theory. I guess I wasn’t confident that intensional TT implies intuitionistic TT, and I have an unfortunate tendency to mix them up (both start with ‘in-‘ I think?)

Show replies