An example showing how to deal with mutually defined data structures.

Example.idr

||| Dependent Types Suck!
|||
||| Sometimes dependent types push you towards mutually defined data
||| structures: I try to avoid them where I can. For me, this occurrs
||| when you need a helper data type where a container is not suitable
||| expressive at the type level to capture the inductive case. When
||| this happens you can index your helper data structure with the
||| signature of the top type. This helps remove the need for a mutual
||| definition, that is turn the call graph edge from being undirected
||| to directed.
|||
||| Here we illustrate the problem and provide a nice solution.
module Example

-- ----------------------------------------------------------- [ Preliminaries ]

{-

First we define some helper containers that exist outside of the
example in public libraries but we include here to keep the example
self-contained.

-}


namespace Vect
  data Vect : (s : Nat)
           -> (e : Type)
           -> Type
    where
      Empty : Vect Z a
      Extend : (head : a)
            -> (tail : Vect k a)
            -> Vect (S k) a

namespace VectD
  ||| A reformulation of a vector of dependent pairs.
  |||
  ||| Analogous to the forall list quantifier.
  data VectD : (a  : Type)
            -> (e  : a -> Type)
            -> (s  : Nat)
            -> (as : Vect s a)
            -> Type
    where
      Empty : VectD a e Z Empty
      Extend : (head : e v)
            -> (tail : VectD a e k vs)
            -> VectD a e (S k) (Extend v vs)

namespace VectP
  ||| A reformulation of a vector of dependent pairs but with an added
  ||| constraint on the parameter/index.
  |||
  ||| Analogous to the forall list quantifier.
  data VectP : (a  : Type)
            -> (e  : a -> Type)
            -> (p  : a -> Type)
            -> (s  : Nat)
            -> (as : Vect s a)
            -> (ps : VectD a p s as)
            -> Type
    where

namespace ListD
  ||| A reformulation of a vector of dependent pairs.
  |||
  ||| Analogous to the forall list quantifier.
  data ListD : (a  : Type)
            -> (e  : a -> Type)
            -> (as : List a)
            -> Type
    where
      Empty : ListD a e v
      Extend : (head : e v)
            -> (tail : ListD a e vs)
            -> ListD a e (v::vs)

-- ------------------------------------------------------------- [ The Setting ]

{-

Here we provide the setting in which our problem and solution must exist.

-}

||| Meta typing
data Meta = A | B String | C (Vect (S n) String)

||| Some important information
data Foo

||| Types
data Ty : (meta : Meta) -> Type where
  Alpha : Ty A
  Oscar : Ty A
  Delta : Nat -> Ty A -> Ty A

  Bravo : (s : String) -> (foo : Foo) -> (b : Bool) -> Ty (B s)

  Charlie : (cs : VectD String (Ty . B) (S n) ss)
         -> Ty (C ss)

||| We define a collection of types as follows.
Types : List Meta -> Type
Types = ListD Meta Ty

-- ------------------------------------------------------------- [ The Problem ]

{-

Our problem comes from wanting to establish a predicate over a given
instance of `Types` such that *all* instances of `Bravo` are set to true.

We will call this predicate: `AllTrueBravos`.

The interesting case is not defining a predicate over `Types` but over
a single instance of `Type`. The interesting case is for `Charlie.

We will call the predicate on a single `Type` instance: `AllTrueBravo`.

We begin by defining an instance for `AllTrueBravo` to see what the problem is.

-}

namespace Problem

  data AllTrueBravo : (type : Ty m) -> Type where
    ||| Any `A` is true.
    AnyATrue : {a : Ty A} -> AllTrueBravo a

    ||| Bravo is true if the `b` field is `True`.
    BravoTrue : AllTrueBravo (Bravo s foo True)

    CharlieTrue : {ss : Vect (S n) String}
               -> {cs : VectD String (Ty . B) (S n) ss}
               -> (prfCSTrue : ?attempOneRhs)
               -> AllTrueBravo (Charlie cs)

{- [ A Question ] What should the type of `?attempOneRhs` be?

Ideally, we should want to use an instance of `VectP` as that gives us
the type:

-}
namespace AttemptOne

  data AllTrueBravoA : (type : Ty m) -> Type where
    ||| Any `A` is true.
    AnyATrue : {a : Ty A} -> AllTrueBravoA a

    ||| Bravo is true if the `b` field is `True`.
    BravoTrue : AllTrueBravoA (Bravo s foo True)

    CharlieTrue : {ss : Vect (S n) String}
               -> {cs : VectD String (Ty . B) (S n) ss}
               -> (prfCSTrue : VectP String
                                     (\s => AllTrueBravoA (Bravo s foo True))
                                     (Ty . B)
                                     (S n)
                                     ss
                                     cs)
               -> AllTrueBravoA (Charlie cs)

{- It type checks! Ship It!

No!

The problem is the unaccounted for `foo`. When you go to write your
decidable procedure, this will cause a unification problem trying to
assert that some foo is equal to another foo, and thus two bravo's
that you know are the same cannot be shown to be the same.

-}

{- [ Attempt Two: A Little Miss-direction can 'help' ]

Let us attemp to fix the problem by spinning out a definition to
capture `BravoTrue` instances for the `CharlieTrue` case.

Here we will need to define a mutual block to capture two mutually
defined data structures.

-}
namespace AttempTwo

  mutual
    data LittleMissDirect : (s : String) -> Type where
      ApplyLMD : {bravo : Ty (B s)}
              -> (prf : AllTrueBravoC bravo)
              -> LittleMissDirect s

    data AllTrueBravoC : (type : Ty m) -> Type where
         ||| Any `A` is true.
         AnyATrue : {a : Ty A} -> AllTrueBravoC a

         ||| Bravo is true if the `b` field is `True`.
         BravoTrue : AllTrueBravoC (Bravo s foo True)

         CharlieTrue : {ss : Vect (S n) String}
                    -> {cs : VectD String (Ty . B) (S n) ss}
                    -> (prfCSTrue : VectP String
                                          (LittleMissDirect)
                                          (Ty . B)
                                          (S n)
                                          ss
                                          cs)
                    -> AllTrueBravoC (Charlie cs)

{- It type checks! Ship It!

No!

We have the same problem as before.

When you go to write your decidable procedure, the miss direction will
cause a unification problem when working on the `ApplyLMD` pattern for
the `CharlieTrue` cases.

We need to ensure that the 'proofs' on `cs` are applied to `cs` and
that there is no ambiguity. Unificiation will be problematic
otherwise.

-}

{- [ Attempt Three: A Little Miss-direction can 'help' Take 2]

Let us attemp to fix the problem by *not* using `VectP` and using a
custom data structrure.

-}
namespace AttempThree

  mutual

    data LittleMissDirect : (cs : VectD String (Ty . B) (S n) ss) -> Type where

      ||| The length is `(S n)` remember.
      Last : (bravo : Ty (B s))
          -> (prf : AllTrueBravoD bravo)
          -> LittleMissDirect (Extend bravo Empty)

      NotLast : (bravo : Ty (B s))
             -> (prf : AllTrueBravoD bravo)
             -> (rest : LittleMissDirect bravos)
             -> LittleMissDirect (Extend bravo bravos)

    data AllTrueBravoD : (type : Ty m) -> Type where
         ||| Any `A` is true.
         AnyATrue : {a : Ty A} -> AllTrueBravoD a

         ||| Bravo is true if the `b` field is `True`.
         BravoTrue : AllTrueBravoD (Bravo s foo True)

         CharlieTrue : {ss : Vect (S n) String}
                    -> {cs : VectD String (Ty . B) (S n) ss}
                    -> (prfCSTrue : LittleMissDirect cs)
                    -> AllTrueBravoD (Charlie cs)


{-

However, we are still in a mutual block. Let us parameterise
`LittleMissDirect` by the type signature of `AllTrueBravoD` to allow
us to remove the need for a mutual block.

-}


{- [ Attempt Four: The Rug that brings it all together]


-}

namespace TheRug

  data LittleMissDirect : (allTrueBravo : (type : Ty m) -> Type)
                       -> (cs : VectD String (Ty . B) (S n) ss)
                       -> Type
    where

      ||| The length is `(S n)` remember.
      Last : (bravo : Ty (B s))
          -> (prf : allTrueBravoD bravo)
          -> LittleMissDirect allTrueBravoD (Extend bravo Empty)

      NotLast : (bravo : Ty (B s))
             -> (prf : allTrueBravoD bravo)
             -> (rest : LittleMissDirect allTrueBravoD bravos)
             -> LittleMissDirect allTrueBravoD (Extend bravo bravos)

  data AllTrueBravoE : (type : Ty m) -> Type where
       ||| Any `A` is true.
       AnyATrue : {a : Ty A} -> AllTrueBravoE a

       ||| Bravo is true if the `b` field is `True`.
       BravoTrue : AllTrueBravoE (Bravo s foo True)

       CharlieTrue : {ss : Vect (S n) String}
                  -> {cs : VectD String (Ty . B) (S n) ss}
                  -> (prfCSTrue : LittleMissDirect AllTrueBravoE cs)
                  -> AllTrueBravoE (Charlie cs)


  data AllTrueBravos : Types ms -> Type where
    Empty : AllTrueBravos Empty
    Extend : (head : AllTrueBravoE type)
          -> (tail : AllTrueBravos types)
          -> AllTrueBravos (Extend type types)

{- [ NOTE ]

When writing the decision procedure for `littleMissDirect` you will
want to first define the procedure signature for `allTrueBravo` first.

-}

allTrueBravo : (type : Ty m) -> Dec (AllTrueBravoE type)

{-

and then realise `littleMissDirect`.

-}

littleMissDirect : (cs : VectD String (Ty . B) (S n) ss)
                -> Dec (LittleMissDirect AllTrueBravoE cs)

{-

and *then* give the procedure body for `allTrueBravos`.

-}

allTrueBravo type = ?allTrueBravo_rhs

{-

Thus, further removing the need for a mutual block, as you will need `allTrueBravo`.

Not to mention that last of all you will want to give the decision procedure for 
`allTrueBravos`.

-}

allTrueBravos : (types : Types ms) -> Dec (AllTrueBravos types)

-- ----------------------------------------------------------------- [ The End ]