Rubrication

For my thesis I've needed to use strictly positive types to avoid the problems which can occur with types of the form: νD. D → D, which were discussed briefly in my post System F is Amazing. In order to ensure types are positive they should be restricted in some way.  It is therefore convenient to have formation rules for types which ensure that we can't make bad types. My starting point was a wonderful paper by Andreas Abel and Thorsten Altenkirch [1] Specifically, this paper describes interleaved inductive types, which is close to what I want.   However, I also want to be able to have polymorphism using ∀.  Since I'm interested in becoming more familiar with Agda (a language in which I'm still a novice) I've written the following as a prototype of my type formation rules, as an experiment. First, we have to set up the appropriate libraries. module StrictlyPositive where open import Data . Nat open import Data . Bool open import Data . List ...

As I mentioned in my last post System-F is amazing. I haven't written in a very long time because I have been busy ensuring that I graduate. I passed my viva finally! So now that I'm back in the real world I thought I'd talk a bit about things that I found while I was in my cave. I'll put my dissertation up with some notes when I've completed the revisions. Those who have dealt with proof assistants based on type theories (Such as Agda and Coq) might have noticed that we often require types to have a positivity restriction. This restriction essentially states that you can't have non-positive occurrences of the recursive type variable. As I described earlier , System F avoids this whole positivity restriction by forcing the programmer to demonstrate that constructors themselves (as a Church encoding) can be implemented, avoiding the problem of uninhabited types being inadvertently asserted . So this means that in some sense positivity is probably the sa...