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

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

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

Replying to

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

This Tweet was deleted by the Tweet author. Learn more

Show replies