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

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.

1:46 AM · Jun 12, 2021Twitter Web App

Replying to

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

Jun 12, 2021

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