One of my favorite parts of programming in strongly typed languages is the
ability to use the type signature of a function to figure out what it does.
For instance, `:t map`

returns either `map :: (a -> b) -> [a] -> [b]`

in
Haskell, or `Prelude.Functor.map : Functor f => (a -> b) -> f a -> f b`

in
idris, both of which make it relatively clear how map works (provided, in the
case of idris, you're at least moderately familiar with what a functor is.)
Both haskellmode-vim and
idris-vim make it very easy to
check types from inside the editor.

Recently when I was working on a project of
mine I
came across two different `all`

s in idris. One is quite intuitive and has
type of `Prelude.Foldable.all : Foldable t => (a -> Bool) -> t a -> Bool`

,
which is quite similar to Haskell's all, which has a type of ```
all :: (a ->
Bool) -> [a] -> Bool
```

, but another one has a type of
```
Data.Vect.Quantifiers.all : ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec
(All P xs)
```

. Yet more confusing is the fact that in idris, `:t All`

(with a
capital 'A') returns ```
Data.Vect.Quantifiers.All : (a -> Type) -> Vect n a ->
Type
```

.

After finding this, I was fairly confused, as my intuitive understanding of
`all`

was that it should take a list-like group of items and return a Boolean
representing whether they all have some certain property. This absolutely
makes sense in with the `all`

defined in Prelude.Foldable and Haskell's all,
but the difference between `Type`

, `Dec (All P xs)`

, and a `Bool`

seemed hard
to reconcile to me.

Doing some more analysis, I decided to start by picking apart `Dec (All P xs)`

.
`:t Dec`

shows `Prelude.Basics.Dec : Type -> Type`

shows that apparently
`Dec`

is a function from a Type to a Type, which isn't necessarily helpful by
itself, but `:doc Dec`

actually is, returning:

```
1 Data type
2 > Dec : Type -> Type
3 Decidability. A decidable property either holds or is a
4 contradiction.
5
6 Constructors:
7 > Yes : (prf : A) -> Dec A
8 The case where the property holds
9 Arguments:
10 > prf : A -- the proof
11
12 > No : (contra : A -> _|_) -> Dec A
13 The case where the property holding would be a contradiction
14 Arguments:
15 > contra : A -> _|_ -- a demonstration that A would be a contradiction
```

Now we're getting somewhere. `Dec`

takes as a parameter a type, but since this
is idris, types and propositions are the same thing, and `Dec`

just states
that either the proposition holds or doesn't. Since the proposition is either
true (it can be shown to hold in this case) or false (it implies a
contradiction if true), `Dec`

will return either `Yes`

or `No`

. This is quite
similar to a standard Bool, but arguably more useful in that it can speak
about general cases and also state both whether the given statement is true or
false, but also in some sense why. For instance idris defines a class `DecEq`

as:

```
1 class DecEq t where
2 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)
```

In some sense this serves the same purpose as `(==)`

(which has a type of
`Prelude.Classes.(==) : Eq a => a -> a -> Bool`

in idris), but because `(==)`

returns a `Bool`

, it can only tell us whether two things are equal, whereas
`DecEq`

can tell us *why* two things are equal.

In fact, `DecEq`

is actually defined on Bools in Decidable.Equality as:

```
1 total trueNotFalse : True = False -> _|_
2 trueNotFalse Refl impossible
3
4 instance DecEq Bool where
5 decEq True True = Yes Refl
6 decEq False False = Yes Refl
7 decEq True False = No trueNotFalse
8 decEq False True = No (negEqSym trueNotFalse)
```

Note the difference between this and the definition of `Eq`

for Bools, which is
simply:

```
1 instance Eq Bool where
2 True == True = True
3 True == False = False
4 False == True = False
5 False == False = True
```

The crucial difference between the two is that while `True == False = False`

says that True and False *are not* equal, `decEq True False = No trueNotFalse`

says True and False *cannot* be equal. Back to the case of lists, if we look
at the definitions of `All`

and `all`

, we find:

```
1 data All : (P : a -> Type) -> Vect n a -> Type where
2 Nil : {P : a -> Type} -> All P Nil
3 (::) : {P : a -> Type} -> {xs : Vect n a} -> P x -> All P xs -> All P (x :: xs)
4
5 notAllHere : {P : a -> Type} -> {xs : Vect n a} -> Not (P x) -> All P (x :: xs) -> _|_
6 notAllHere _ Nil impossible
7 notAllHere np (p :: _) = np p
8
9 notAllThere : {P : a -> Type} -> {xs : Vect n a} -> Not (All P xs) -> All P (x :: xs) -> _|_
10 notAllThere _ Nil impossible
11 notAllThere np (_ :: ps) = np ps
12
13 all : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a) -> Dec (All P xs)
14 all _ Nil = Yes Nil
15 all d (x::xs) with (d x)
16 | No prf = No (notAllHere prf)
17 | Yes prf =
18 case all d xs of
19 Yes prf' => Yes (prf :: prf')
20 No prf' => No (notAllThere prf')
```

This is now much clearer (at least to me.) `all`

takes a proposition, a way to
verify that proposition, and a list of things, and returns why the proposition
does or doesn't hold for everything in the list. It's the difference between
a multiple-choice and short-answer question, in that while they can state the
same thing, the answer to one is much more helpful in reasoning about future
questions than the other. While a Bool is fine for simple questions, there's
a lot to be gained from using `Dec`

when it's practical.

One of the more interesting applications for this is this quasigroup completion solver, later adapted to a benchmark of idris itself. A quasigroup is just a set for and an operation such that each element of the set appears exactly once in each row and column of the Cayley Table generated from the elements in the set and the operation. This property also means that the quasigroup completion problem is often referred to as the Latin Square problem, since said Cayley table is also a Latin Square by definition. It is a common combinatorial problem to take a given partially filled Latin Square and complete it in a way consistent with the definition. This process is actually quite similar to sudoku, where a grid of spaces that are either empty or containing a value are given, and the goal is to fill in the empty squares so that the same number does not appear twice in any row or column. Of course, quasigroup completion is a more general and abstract problem, but the fundamental process is the same.

The solver shown uses the Data.Vect.Quantifier version of `all`

to reason about
things like whether given rows and columns are "safe" to place an element in,
perhaps most notably in the definition of legalVal, which is used to evaluate
whether a given cell assignment is "legal" with regard to the definition of
quasigroup.

```
1 LegalVal : Board n -> (Fin n, Fin n) -> Fin n -> Type
2 LegalVal b (x, y) val = (Empty (getCell b (x, y)), All (LegalNeighbors (Just val)) (getCol x b), All (LegalNeighbors (Just val)) (getRow y b))
3
4 legalVal : (b : Board n) -> (coord : (Fin n, Fin n)) -> (val : Fin n) -> Dec (LegalVal b coord val)
5 legalVal b (x, y) v =
6 case rowSafe b y v of
7 No prf => No (\(_, _, rf) => prf rf)
8 Yes prf =>
9 case colSafe b x v of
10 No prf' => No (\(_, cf, _) => prf' cf)
11 Yes prf' =>
12 case empty (getCell b (x, y)) of
13 No prf'' => No (\(ef, _, _) => prf'' ef)
14 Yes prf'' => Yes (prf'', prf', prf)
```

In the definition of `legalVal`

, `prf`

, `prf'`

, and `prf''`

all refer to proofs
of the "safety" of the given value at the given coordinates with respect to
its row, column, and occupancy status. This allows `LegalVal`

to be a type
that only represents legal values, and thus guarantee that functions using
that type can only ever give legal values, because otherwise the program would
type check. Not that this is totally impossible in a language like Haskell
with no dependant types, as you cannot have a function like `LegalVal`

to a
type, and hence the type cannot *depend* on parameters that aren't other
types, and hence can't carry guarantees about them like in a language like
idris.

This makes our initial question of the behavior of the two `all`

s much simpler.
One returns either True or False, and the other returns either `Yes`

or `No`

,
but the second provides a reason for the returned value that can be used to
reason about the behavior of the program in general and guarantee certain
behaviors.