## Stay Positive with Your Data Types

In this blog post, we will investigate the notion of strictly positive inductive data types, which is a condition that Juvix mandates for a data type to be considered well-typed.

An **inductive type** is considered *strictly positive* if it either:

- Does not appear within the argument types of its constructors, or
- Appears strictly positively within the argument types of its constructors.

A name is considered strictly positive for an inductive type if it never appears
in a negative position within the argument types of its constructors. The term
*negative position* denotes instances located to the left of an arrow in a type
constructor argument.

### Example

Consider the following data type `X`

where `A`

and `B`

are types in scope:

```
type X :=
| c0 : (B -> X) -> X
| c1 : (X -> A) -> X;
```

In this example, the type `X`

occurs strictly positive in the constructor `c0`

,
but negatively in the constructor `c1`

in the type argument `X -> A`

. Therefore,
`X`

is not strictly positive.

Positive parameters can also be described as those that do not occur in negative
positions. For instance, the type `B`

in the `c0`

constructor above appears to
the left of the arrow `B->X`

, placing `B`

in a negative position. It is
essential to consider negative parameters when verifying strictly positive data
types, as they might enable the definition of non-strictly positive data types.

Let us consider another example:

```
type T0 (A : Type) :=
| c0 : (A -> T0 A) -> T0 A;
```

```
type T1 :=
| c1 : T0 T1 -> T1;
```

In this example, the type `T0`

is strictly positive, while the type `T1`

is not.
It is only after unfolding the type application `T0 (T1 A)`

in the data
constructor `c1`

that we can determine `T1`

occurs in a negative position due to
`T0`

. More specifically, the type parameter `A`

of `T0`

is negative.

### Bypassing the Strict Positivity Condition

To bypass the positivity check in a data type declaration, you can annotate it
with the `positive`

keyword. Alternatively, you can use the CLI global flag
`--no-positivity`

when type checking a `Juvix`

file.

```
positive
type T0 (A : Type) :=
| c0 : (T0 A -> A) -> T0 A;
```

### Examples of Non-Strictly Positive Data Types

- The
`Bad`

data type is not strictly positive due to the negative parameter`A`

of`Tree`

.

```
type Tree (A : Type) :=
| leaf : Tree A
| node : (A -> Tree A) -> Tree A;
```

```
type Bad :=
| bad : Tree Bad -> Bad;
```

`A`

is a negative parameter.

```
type B (A : Type) :=
| b : (A -> B (B A -> A)) -> B A;
```