[Agda] Parameterized type families

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Nils Anders Danielsson wrote:
>>> See the Agda wiki:
>>> http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Docs.DatatypeAndFunctionDefinitions.
>>>
>>
>> There's a little opaque type-theoretic jargon there. What does
>> 'negative' mean? On the LHS of an arrow?
> 
> Negative:          To the left of an odd  number of arrows.
> Positive:          To the left of an even number of arrows.
> Strictly positive: To the left of zero              arrows.
> 
>> Presumably it's called that because it means its argument is being
>> 'destroyed' or 'destructed', while on the RHS it's being 'created' or
>> 'constructed' so is positive?

I guess it comes from logic:

  not A        is a negative statement
  not (not A)  is doubly-negative (hence positive)

In constructive logic,

  not A  =  A -> False

Your view fits in here.

In the context of linear logic, positivity/negativity has been studied
extensively under the term "polarity".

Cheers,
Andreas

- --
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFJBMO6PMHaDxpUpLMRAq64AJ9FC/IJ+9YQdDwk6ucH8LKrnXjBCQCfR+tT
5B57CiAarDK/Ez6XPc2FLrY=
=Y59W
-----END PGP SIGNATURE-----