[Agda] Positivity checker

[Nils Anders Danielsson]

On 2008-12-07 21:45, Peter Dybjer wrote:
>
> The reason why this data type is ok, is because it is isomorphic to the 
> corresponding family defined by induction on n.
> 
> But what is the induction principle? Except induction on n?

Do you suggest that one could inadvertently introduce new (stronger)
induction principles by accepting this type (or similar types)?

> On Dec 5, 2008, at 4:53 PM, Nils Anders Danielsson wrote:
>
>> On 2008-12-04 17:31, Wouter Swierstra wrote:
>>
>>> but I'd much rather work with data (the example I have in mind is
>>> pretty complicated).
>>
>> Yes.
> 
> Why?

We have already had this discussion:

 
http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Main.InductiveFamilies

The list archives may be more persistent than the wiki, so I include
parts of my contribution to that discussion:

   The Vec example has been discussed above. While it is possible to
   define vectors using a function, do we want to do that? The Vec type
   is often seen as a more precise version of the List type, and this is
   most easily seen when they are both defined as data. [If the only two
   choices are the standard data type and the standard Set-valued
   function.] I don’t think we should scare away functional programmers,
   who are familiar with data types (and now also GADTs), by defining Vec
   in a different way from List.

   Furthermore, when functions are defined by explicit recursion,
   functions defined over Vec defined as a function are quite a bit more
   verbose than those defined over Vec defined as an inductive family:

    map : forall {a b n} -> (a -> b) -> Vec a n -> Vec b n
    map f []       = []
    map f (x ∷ xs) = f x ∷ map f xs

    map' : forall {a b} n -> (a -> b) -> Vec' a n -> Vec' b n
    map' zero    f tt       = tt
    map' (suc n) f (x , xs) = f x , map' n f xs

   It also feels wrong to pattern match on a pair, when I want to pattern
   match on a cons. This can be worked around as follows (based on code
   written by Ulf):

    data Nil : Set where
      nil : Nil

    data Cons (A As : Set) : Set where
      _::_ : A -> As -> Cons A As

    Vec : Set -> Nat -> Set
    Vec A  zero   = Nil
    Vec A (suc n) = Cons A (Vec A n)

    map : forall {a b} n -> (a -> b) -> Vec a n -> Vec b n
    map zero    f nil       = nil
    map (suc n) f (x :: xs) = f x :: map n f xs

   Finally Vec defined as a function has a tendency to be harder to work
   with, since the definition unfolds when the natural number is not
   neutral. There is a workaround for this as well, adding even more
   overhead (code by Ulf):

    -- When defining types by recursion it is sometimes difficult to
    -- infer implicit arguments. This module illustrates the problem and
    -- shows how to get around it for the example of vectors of a given
    -- length.

    module Introduction.Data.ByRecursion where

    data Nat : Set where
      zero : Nat
      suc  : Nat -> Nat

    data Nil : Set where
      nil' : Nil

    data Cons (A As : Set) : Set where
      _::'_ : A -> As -> Cons A As

    mutual
      Vec' : Set -> Nat -> Set
      Vec' A  zero   = Nil
      Vec' A (suc n) = Cons A (Vec A n)

      data Vec (A : Set)(n : Nat) : Set where
        vec : Vec' A n -> Vec A n

    nil : {A : Set} -> Vec A zero
    nil = vec nil'

    _::_ : {A : Set}{n : Nat} -> A -> Vec A n -> Vec A (suc n)
    x :: xs = vec (x ::' xs)

    map : {n : Nat}{A B : Set} -> (A -> B) -> Vec A n -> Vec B n
    map {zero}  f (vec nil')       = nil
    map {suc n} f (vec (x ::' xs)) = f x :: map f xs

To summarise: In Agda it is more convenient to program using data types.

-- 
/NAD


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.