Skip navigation

While working over the weekend with Chris Casinghino and Vilhelm Sjöberg at U. Penn. and Garrin Kimmell here at Iowa on the Trellys core language design and prototype implementation, I had occasion to recall a very tricky way in which too liberal datatype definitions can lead to inconsistency, even if we do not assume a terminating recursor for all datatypes.  I believe I learned this trick from Benjamin Wack, although at this point I am not sure.  The code (in our new Trellys core-language syntax) is here:

data Empty -> Type 0 where
 {}

data Loop -> Type 0 where
 CLoop : (f:((b:Loop) => Empty)) => Loop

prog loop_step : (b : Loop) => Empty

loop_step = \ b . case b [beq] of CLoop f -> f b

prog loop : Empty

loop = loop_step (CLoop loop_step)

 

Notice that this example does not use any explicit recursion (rec or recnat in Trellys), but yet manages to define empty of type Empty.  It can only do that as indeed it does, by writing an infinite loop.  The trick here is to say that the constructor CLoop for the Loop type takes in a function from Loop to Empty as its argument.  Terminating type theories like Coq do not allow this, nor does the logical fragment of the Trellys core language.  Constructors that take in arguments whose types mention the type being constructed in a negative position must take those arguments in as programmatic arguments, rather than logical arguments.  Trellys distinguishes programmatic terms from logical ones, while allowing the two to interact.  The above example is programmatic, as shown by the use of the thick arrow in several places, and the “prog” keyword for loop_step and loop.  The thick arrow means that the input may be programmatic.  A thin arrow for function types means that the argument can only be logical, not programmatic.  If we replace the thick arrows above with thin ones and drop “prog”, the example will not type check (at least, it won’t as soon as Chris and/or Vilhelm implement the positivity check :-)).

Anyhow, I thought it was worthwhile to share this example, since it shows that datatypes which are fine for programming can be dangerous for logic, even if we do not assume a terminating recursor for them.

About these ads

2 Comments

    • Artyom Shalkhakov
    • Posted October 15, 2010 at 10:42 am
    • Permalink
    • Reply

    Could you elaborate more on positivity restriction (and more generally, on “negative/positive data type occurrences”)?

    I’ve found uses of this term over the web, but no explanation really. Is there something basic I am missing?

    I’ve picked up “Inductive Definitions in the System Coq Rules and Properties” by Christine Paulin-Mohring.

    Right now, I am thinking that a datatype D is positive, informally, if none of its constructors contain occurrences of D to the left of the arrow if we look at the signatures of the datatype constructors.

    • Hi, Artyom. Take a look at Section 3 of “Inductively Defined Types in the Calculus of Constructions” by Pfenning and Paulin-Mohring, which you can find here (Citeseer). The give a formal definition of when a variable occurs only positively and when only negatively in a type expression. Basically,the positivity requirement for a datatype x is that for each constructor c of type T1 -> … Tn -> x, we can only have x to the left of an arrow an even number of times in each Ti. I believe strict positivity is the requirement that x must be to the left of an arrow 0 times. So this is similar to what you are saying.


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

Follow

Get every new post delivered to your Inbox.

%d bloggers like this: