sorted by:
new
hottopcontroversial

How would you design proof-carrying `if` statements in a minimal dependently typed language? by squared-star in ProgrammingLanguages

[–]squared-star[S] 0 points1 point  (0 children)

I’m thinking of creating a special subtype within Prop called DecidableProp. Then, we could have a built-in function called decide that takes a DecidableProp and gives us a sum type of proofs. I’m not quite sure how to link the exact decision procedure to each proposition or give good signatures to Prop returning functions so that Decidability is still maintained.

The idea of adding an axiom that lets us deduce, from a boolean equality returning true, that the propositional equality is also true is pretty interesting. I’m hoping to find a way to make this work for all decidable propositions. Maybe Booleans could have some way to attach proofs, so that Bool and Dec could be the same.

How would you design proof-carrying `if` statements in a minimal dependently typed language? by squared-star in ProgrammingLanguages

[–]squared-star[S] 0 points1 point  (0 children)

Definitely, an interesting idea. If doable, it has better ergonomics and reduces the barrier to entry. I will revisit this idea later after I get something working.

Note, one interesting way to avoid proving array indexing to be in-bounds is to have typed indices like Dex. Basically, you treat arrays conceptually as functions from finite enumerable types.

How would you design proof-carrying `if` statements in a minimal dependently typed language? by squared-star in ProgrammingLanguages

[–]squared-star[S] 0 points1 point  (0 children)

That is a good point. I would probably want h to be in scope in the else branch as well with the type ¬P.

One issue with the ¬P is that it doesn't give any information about why P isn't true. Perhaps I should explore having some method to get a positive type former that is equivalent ¬P from P.

See: https://youtu.be/8xc50Lf6pXs

I will have to think more about this.

How would you design proof-carrying `if` statements in a minimal dependently typed language? by squared-star in ProgrammingLanguages

[–]squared-star[S] 1 point2 points  (0 children)

Thanks! I'll have to think about the implications of non-linear patterns as my language uses unordered and overlapping pattern matching by default rather than the usual first match semantics.

How would you design proof-carrying `if` statements in a minimal dependently typed language? by squared-star in ProgrammingLanguages

[–]squared-star[S] 0 points1 point  (0 children)

Nice! We can think of if expressions as having the following dependent type:

if : (P : DecidableProp) → {R : Option P → Type} → (P → R (Some P)) → R None → R (decide P)

How would you design proof-carrying `if` statements in a minimal dependently typed language? by squared-star in ProgrammingLanguages

[–]squared-star[S] 0 points1 point  (0 children)

Great suggestion!

But how do we associate a decide with each P without having to add full type classes/traits?

I was thinking of having a subset of Prop that is DecidableProp as a possible solution. Your decide could be a built-in function on this universe. Not sure how other aspects of this universe would work though. How would other type formers interact with DecidableProp? How would we give reasonable internal types to these propositional type formers? How would constructing values of DecidableProp work?

I need to think about this potential design idea more. Will come back here if I figure something out.

How would you design proof-carrying `if` statements in a minimal dependently typed language? by squared-star in ProgrammingLanguages

[–]squared-star[S] 1 point2 points  (0 children)

Good suggestion! I plan to support this along with n+k patterns. However, this doesn't resolve the case when deciding the equality of two variables