Jon Sterling comments

Results 198 comments of


                                            Jon Sterling

smalltt

I am expecting that some of Andras's ideas will indeed be applicable :) I'm excited to study it.

Let equate_ty (quote_ty, equiv_ty) handle the types directly

@favonia Is the idea to have a separate quotation function for types, rather than piggy-backing on the universe? Or something else?

Let equate_ty (quote_ty, equiv_ty) handle the types directly

@favonia Gotcha! I think it sounds plausible... Step 2 of the rectification campaign is to use less U_omega, and start using DownX for types as well. I think I still...

Consider using lists instead of splay trees for contexts

Yes, the profiling I've done so far suggests that splay trees are not providing us a performance benefit over lists for our application.

Consider using lists instead of splay trees for contexts

@favonia I think the majority of the culprits lie in `sml-typed-abts` and maybe `sml-dependent-lcf`.

Factor out Favonia Namespace code into library

Good question! We usually work on branches in the main repo rather than forks.

Concrete notation of coe sucks!

Carlo and I trained our prethought on this for a few hours and are very discouraged. Everything we could come up with sucks in some way or another... We'll come...

Log levels for output hygiene

Ideally, nothing should be emitted that the user doesn't ask for.

Useless(?) hComp’s with empty systems when using higher inductive types

@coquand Thank you for the very helpful comments. I have a question about this failure of confluence... My understanding of the operational interpretation (as in Simon's paper) of cubicaltt is...

Useless(?) hComp’s with empty systems when using higher inductive types

@coquand The operational semantics of S1 elimination would proceed as usual when its principal argument is a value—the only difference is that under the discussed circumstances, `hcomp S1 base []`...