1

I would like to test some definitions in system F using Agda as my typechecker and evaluator.

My first attempt to introduce Church natural numbers was by writing

Num = forall {x} -> (x -> x) -> (x -> x)

Which would be used just like a regular type alias:

zero : Num
zero f x = x

However the definition of Num does not type(kind?)check. What is the most proper way to make it working and be as close as possible to the system F notation?

radrow
  • 6,419
  • 4
  • 26
  • 53
  • 1
    What is the error? What if you place `{-# OPTIONS --type-in-type #-}` at the top of the file? – effectfully Jun 06 '19 at 14:27
  • The error I get for this particular example is `piSort (univSort _3) (λ _ → piSort (piSort _3 (λ _ → _3)) (λ _ → piSort _3 (λ _ → _3))) !=< Set → Set of type univSort (piSort (univSort _3) (λ _ → piSort (piSort _3 (λ _ → _3)) (λ _ → piSort _3 (λ _ → _3)))) when checking that the expression ∀ {x} → (x → x) → x → x has type Set → Set` – radrow Jun 06 '19 at 15:07

1 Answers1

2

The following would typecheck

Num : Set₁
Num = forall {x : Set} -> (x -> x) -> (x -> x)

zero : Num
zero f x = x

but as you see Num : Set₁, this might become a problem and you'll need --type-in-type

Saizan
  • 1,391
  • 8
  • 4