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

Andrej Bauer

@andrejbauer

Jun 12, 2021

I always understood the refinment types as dependent types with a computationally irrelevant component that gets erased. Is that too naive? I know

@noamzoam

will admonish me for saying this :-)

Brendan Zabarauskas

@brendanzab

Jun 12, 2021

I'm wondering if instead of being erasured, you could just have them be restricted to elaboration time, seeing as that's when you'd have access to a solver. Perhaps something like staging could be used? It think that might be what Jon is getting at here: twitter.com/jonmsterling/s

This Tweet is unavailable.

Replying to

and

And it might help to have some way of restricting those refinements to be in a subset of things supported by your solver? But I'm not sure. 😅

7:48 AM · Jun 12, 2021Twitter Web App