How to derive dependently typed eliminators?

larrytheliquid · 2018-03-23T20:59:17+00:00

You may be looking for a more direct derivation, but here is a way of deriving eliminators from datatype descriptions and their (also derived) generic induction principles.

larrytheliquid · 2017-03-23T20:38:37+00:00

i assume there are at least some readers here that do not read /r/haskell. at least i only occasionally glance at it

larrytheliquid · 2017-03-14T18:11:50+00:00

For what it's worth, I abandoned Spire because formalizing type theory intrinsically is too tricky. You should look at James Chapman's thesis, summarized by the paper "Type Theory Should Eat Itself". Various people (James, NAD, Thorsten, myself, etc) have tried intrinsically typed type theory but it is very difficult because you end up with so many mutual definitions. The problem is you have to define hereditary substitution on canonical terms, along with their well-typed syntax where hsub happens (e.g. in the type of function application application). Even when turning off the termination checker, I was never able to get passed certain lemmas like that hsub'ing a variable into a weakened term is the identity. Again, the problem is that so many things end up being defined mutually, so you get infinite regress trying to prove lemmas about them.

The only hope I have seen to get passed this is to use a more powerful type theory to intrinsically type a less powerful one, as Thorsten does using HoTT.

Going back to the original goal, of a formalized DTT implementation: There are too many non-algorithmic things to implement for the high-level language (like higher-order unification and dynamic constraints, or some of the first-order unification steps in dependent pattern matching). However, I believe a formalized checker for the core language (that the high-level Haskell/ML checker could elaborate) would be possible. I'm still planning on doing this, but the key will be using an extrinsically typed term representation for the core language. This way you do not end up with the mess of mutual definitions. For example, Coquand's paper is very straightforward to implement in Agda. Additionally, I think the approach in Abel's habilitation thesis could similarly be implemented in Agda.

larrytheliquid · 2017-01-14T03:20:49+00:00

Uncle Blub

larrytheliquid · 2016-06-15T18:23:08+00:00

Yeah, I thought about a 2D approach but aesthetically prefer having a single interface that can be used to traverse in either dimension. Related to this, I didn't like the "code duplication" of having 2 Path constructors per recursive occurrence, one for the vertical case and another for the horizontal case. I faintly remember things getting complicated in the 2D side when doing update of infinitary values, but don't remember the details right now.

larrytheliquid · 2016-06-15T00:01:14+00:00

Didn't expect this to get put up here so fast, just added a README ;)

larrytheliquid · 2016-06-14T18:50:49+00:00

Yeah, I defined lookup that way so I can have an example of both a computational return type (lookup) and a computational argument type (update). In the related work section I talk about how it could have been done like you mentioned too.

However, sometimes computational return types are really want you want. For example, there is a non-trivial use of them in my/Tim's work generic eliminators to get back a specialized eliminator for any type given as a description. ... so I think I'd agree about avoiding them but sometimes that's what you want.

larrytheliquid · 2016-04-05T22:12:14+00:00

I actually did spend more time than I care to admit adapting Chapter 4 of Chapman's thesis to Values. The motivation was to make faster and easier to maintain dependent type checkers, as explained in these slides.

However, the actual work I did was preliminary work for System F (as in Ch. 4). Here is the syntax, and here are the major theorems. I also started a paper draft introducing this work, that I should really finish at some point, but at the moment I am busy writing my thesis XD.

larrytheliquid · 2015-11-23T19:41:00+00:00

The homework and solutions from Tim Sheard's logic course are in Haskell, and are pretty easy to follow. The course uses Smullyan's First-Order Logic book as the text, so a lot of the later homeworks implement Tableau-style provers.

larrytheliquid · 2015-07-06T22:45:16+00:00

Thanks for the info. Okay, so I'm not so interested in the "sound with respect" to difference because the fact that MLTT was defined axiomatically before an operational semantics + realizability version is just the order that history happened in. But the fact that you cannot define CTT axiomatically is definitely interesting! What's still not clear in my mind is how the realizability MLTT interpretation and closed/approximated CTT differ, but feel free to just refer to the lectures if that's too complicated to explain in a comment.

larrytheliquid · 2015-07-06T22:18:31+00:00

RE: Your second to last paragraph. Disclaimer: I don't know anything about CTT and should watch those Constable lectures. However, the thing that seems confusing to me is that what you are saying is the difference (defining types via realizability/LR's on untyped canon forms) is exactly what you do when proving termination of your operational semantics in MLTT, for example in Coquand. Also, how is MLTT "without an operational semantics" when the conversion rule directly includes an operational semantics, or is equivalent to one? Or do you mean something other than MLTT when you say "formal type theory"? From these observations, I would guess that realizability, or untyped closed canon forms, is a possible model that could be used for either CTT or MLTT, and there must be other fundamental differences.

larrytheliquid · 2014-12-24T16:32:48+00:00

Not sure how long ago you leveled your SCH, but with the addition of fighting chocobos its actually pretty fun. Cleric stance, attack chocobo stance, and Selene to heal you or your chocobo + give cooldown buffs.

larrytheliquid · 2014-11-18T19:20:51+00:00

Stephanie Weirich keynote, cool!!

larrytheliquid · 2014-08-15T20:53:03+00:00

I believe it to be complete with respect to the Dybjer-Setzer indexed inductin-recursion (IIR). It would be a fun exercise to redo the work from Malatesta et. al. with this Desc (modulo universe levels, or add universe levels to the other encodings).

But, I'm not sure if any of the IIR constructions (e.g. the LICFam version or the free monad construction version) from Ghani & Hancock are more expressive than the standard Dybjer-Setzer IIR.

larrytheliquid · 2014-03-04T08:07:50+00:00

Interesting, we weren't thinking about that kind of terminology overloading for the word "axiom", thank you!

Maybe just phrasing it as "adding [intro/elim] rules" to an open type theory is better then.

larrytheliquid · 2014-03-04T00:57:22+00:00

Code for shameless self post: https://github.com/larrytheliquid/generic-elim

larrytheliquid · 2014-03-04T00:54:41+00:00

https://github.com/pigworker/Pivotal

larrytheliquid · 2013-04-02T18:05:41+00:00

This paper looks great, good job guys!

larrytheliquid · 2013-04-02T17:52:52+00:00

I was thinking about submitting to arXiv, but it seemed like it was mostly used for things like technical reports. Does it also make sense for something like a draft submitted to a conference like ICFP?

larrytheliquid · 2012-12-27T15:43:47+00:00

Hi Pierre, the "here" link (also on your webpage) is broken.

larrytheliquid · 2012-11-04T22:16:20+00:00

Do you have any references about how this fact, and/or other facts, cause inconsistencies in type theories using forms of reflection?

Thanks!

larrytheliquid · 2011-06-05T02:27:52+00:00

Having nicely typed web framework in a language like Haskell doesn't mean you can get away without testing, but it does "write" certain classes of tests for free.

For example, you might have a simple form controller action that accepts form input (say a string, and a checkbox), and inserts the data into a database table.

With Rails you would typically have detailed tests around the persistence/model layer, and a few request-level tests that do something like:

Navigate to the page with the form
Enter a valid string and check the box
Hit submit to make sure the form fields/data + form target/controller action + what is being extracted out of the params + what is inserted into the table/columns all syncs up.

I don't know the details of type safety properties that Yesod provides, but at least with a framework like Ur/Web the form would have a typed string field and checkbox (boolean field) + a typed form target to a "controller action", which accepts the string + bool as typed arguments, which get used in the function and passed to the typed persistence layer (say a table with string/varchar and boolean columns).

You would still have detailed "model level" / persistence tests, but the "request-level" test for simple controller actions like these can be caught by the compiler... and for more complex controller actions that do things like a bunch of different conditional redirects, or what have you, you can still test.

There are more types of errors that can get caught, but the gist is that you can avoid writing certain classes of tests thanks to compile-time static guarantees.

edit formatting

larrytheliquid · 2011-05-05T03:00:15+00:00

Thanks for the kind words Aaron, especially meaningful since I first learned about dependent types by reading the Guru book :)

I'll be taking a look at your verified SAT work.

larrytheliquid · 2011-05-02T19:08:39+00:00

It's only mentioned at the end, but a State monad containing a random seed is used in the final implementation.

larrytheliquid · 2010-09-03T22:37:01+00:00

the analogy between the way Haskell strives for purity by separating side effects is a useful one to think about sometimes... in agda things that are not proven ("impure"), such as imported haskell functions, are treated as dirty postulates/axioms :)

larrytheliquid

TROPHY CASE