How to understand the type declaration and definition for List and Vect in Idris lang?

Question

In Idris doc there are the following lines:

data List a = Nil | (::) a (List a)

data Vect : Nat -> Type -> Type where
   Nil  : Vect Z a
   (::) : a -> Vect k a -> Vect (S k) a

I assumed line 1 is a type definition for List and the rest is type declaration for Vect. I thought there should be both declaration and definition so I looked in the Idris repo and found:

data List : (elem : Type) -> Type where
  Nil : List elem
  (::) : (x : elem) -> (xs : List elem) -> List elem

Which shares a similar pattern with type declaration of Vect so it seems fine. but I cannot find data List a = Nil | (::) a (List a) in souce code. Also, I cannot find type definition for Vect.

So, my confusions are:

Why I can't find data List a = Nil | (::) a (List a) in source code?
What's the actual type definition for Vect?

Alexey Romanov Alexey Romanov · Accepted Answer · 2019-11-19T09:31:10

There are no separate "type definition" and "type declaration" in Idris; these are just two ways to write a type definition. See the Syntax Guide:

Idris provides two kinds of syntax for defining data types. The first, Haskell style syntax, defines a regular algebraic data type...

The second, more general kind of data type, is defined using Agda or GADT style syntax. This syntax defines a data type that is parameterised by some values (in the Vect example, a value of type Nat and a value of type Type).

GADTs were introduced by Haskell, and reading e.g. https://en.wikibooks.org/wiki/Haskell/GADT or searching for GADT can give you additional explanations of the second style.

The GADT-style definition of List is equivalent to the data List a = ... one except for allowing to name elem, x, and xs.

How to understand the type declaration and definition for List and Vect in Idris lang?

1 Answers