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

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

Replying to

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

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

Replying to

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.

Show replies

Replying to

You might find it interesting

github.com

GitHub - 0xd34df00d/refinedt: Refinement types + dependent types =

Refinement types + dependent types =

. Contribute to 0xd34df00d/refinedt development by creating an account on GitHub.

Brendan Zabarauskas

@brendanzab

Jun 12, 2021

Oh thanks! This seems like it might be similar to what I was hoping for, but I'll have to look closer at it!

Show replies

Replying to

Check out F*. It may be what you’re looking for.

Replying to

you might be interested in William Lovas' PhD thesis, "Refinement types for logical frameworks" kilthub.cmu.edu/articles/thesi, as well as an old paper by Frank Pfenning of the same name cs.cmu.edu/~fp/papers/rlf

kilthub.cmu.edu

Refinement Types for Logical Frameworks

The logical framework LF and its metalogic Twelf can be used to encode and reason about a wide variety of logics, languages, and other deductive systems in a formal, machine-checkable way. Recent...

Replying to

I haven't looked at it but your tweet reminded me of this project's description github.com/0xd34df00d/ref :)

github.com

GitHub - 0xd34df00d/refinedt: Refinement types + dependent types =

Refinement types + dependent types =

. Contribute to 0xd34df00d/refinedt development by creating an account on GitHub.

Brendan Zabarauskas

@brendanzab

Jun 14, 2021

Yeah I got recommended this in another subthread! I think the surface language might be more limited than what I'd hope for though - not sure how hard that would be to change though.

Quote Tweet

Evgenii Akentev

@ak3n

· Jun 12, 2021

Replying to @brendanzab

You might find it interesting github.com/0xd34df00d/ref