functional-programmingagdatype-theory

Returning the type of a constructor by a function


I am trying to write a simple tuple type

open import Agda.Builtin.List

mutual
  f : List Set -> Set
  f T = g T T where
    g : List Set -> List Set -> Set
    g [] T = Tuple T
    g (t ∷ rest) T = t -> g rest T

  data Tuple (A : List Set) : Set where
    MkTPL : f A

but agda-mode keeps giving me this error:

The target of a constructor must be the datatype applied to its
parameters, playground.g A A A isn't
when checking the constructor MkTPL in the declaration of Tuple

Clearly f A is a function type whose target is Tuple A

Is there any way to tell the compiler that the code is correct (atleast I believe it is)

Also, why does it say playground.g A A A, not playground.g A A?


Solution

  • The constructors of a data type must have a fixed, known number of arguments, so your approach is not going to work. See Data.Product.Nary.NonDependent for a definition of heterogeneous tuples in the standard library.

    Also, why does it say playground.g A A A, not playground.g A A?

    That is because g is defined in scope of T : List Set, so it gets lambda-lifted to a function with three arguments of type List Set. Compare your definition with:

      f : List Set -> Set
      f T = g T where
        g : List Set -> Set
        g [] = Tuple T
        g (t ∷ rest) = t -> g rest
    

    Now Agda reports playground.g A A.