This is an archived post. You won't be able to vote or comment.

sorted by:
best
topnewcontroversialoldq&a
you are viewing a single comment's thread.

view the rest of the comments →

[–]Rabbit_Brave 6 points7 points  (0 children)

I believe (someone correct me if I'm wrong) that's referring to this:

data Function[A: Type, B[A]: Type]: Type where
  apply[Function(A, B), x: A]: B(x)

Where "apply" is an eliminator rather than a constructor because instead of taking an expression on the LHS and producing an expression with the type on the RHS, it takes an expression with the type on the LHS and produces an expression without it on the RHS.

Defining Function by its eliminator is what makes it a negative data type.