[Agda] Strictly positive

[gallais]

There are different ways to achieve this:

* you could either use a datatype describing the functors and
a decoding function taking an element of such a datatype to a
Set -> Set function (see PlainDesc in [1]). Agda will then be
able to "see" that the whole thing is strictly positive. You
can recover the usual constructor-oriented syntax by using
pattern synonyms. Here is a quick demo:
https://gist.github.com/gallais/699274bc576f5040faf0

* or you could use a language where polarity annotations are
part of the type system. MiniAgda [2] is such a language. To
have a minimal syntax highlighting and C-c C-l bound to the
"typecheck this please" command you are used to in Agda, you
may want to install my (unofficial) MiniAgda mode for emacs [3].

Cheers,

[1] Conor McBride, Ornamental Algebras, Algebraic Ornaments
[2] http://www2.tcs.ifi.lmu.de/~abel/miniagda/
[3] https://github.com/gallais/MiniAgda-mode

On 23/02/15 08:15, Kenichi Asai wrote:
> I am trying to encode in Agda the two-level types as introduced by
> Sheard and Pasalic [1].  For example, I can encode the type for simple
> types as follows:
>
> ----------------------------------
> module main where
>
> data t (Type : Set) : Set where
>    TInt : t Type
>    TArrow : Type -> Type -> t Type
>
> data fix : Set where
>    Fix : t fix -> fix
> ----------------------------------
>
> where the parameter "Type" for t shows where the recursion occurs
> (i.e., the two arguments of TArrow).  Now, I want to generalize t
> to an arbitrary type (so that it can be given by users later).  I
> considered:
>
> ----------------------------------
> module Test (t : Set -> Set) where
>
> data fix : Set where
>    Fix : t fix -> fix
> ----------------------------------
>
> but Agda complains:
>
>> fix is not strictly positive, because it occurs in an argument to a
>> bound variable in the type of the constructor Fix in the definition
>> of fix.
> Sure, if I instantiate t to:
>
> t : Set -> Set
> t Type = Type -> Type
>
> it does lead to inconsistency.  But my intention is that I instantiate
> t always as something that is strictly positive in its argument (like
> the t for simple types above).  Is there any way to declare so, so
> that fix can be defined independently of the definition of t?
>
> Thank you in advance.
>
> Sincerely,
>
> [1] Tim Sheard and Emir Pasalic
> "Two-level types and parameterized modules"
> Journal of Functional Programming, 14(5):547-587, September 2004.
>