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 undirected to directed.
Here we illustrate the problem and provide a nice solution.
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.
A reformulation of a vector of dependent pairs. Analogous to the forall list quantifier.
A reformulation of a vector of dependent pairs but with an added constraint on the parameter/index. Analogous to the forall list quantifier.
A reformulation of a vector of dependent pairs. Analogous to the forall list quantifier.
The Setting
Here we provide the setting in which our problem and solution must exist.
Meta typing
Some important information
Types
Context
We define a collection of types as follows.
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.
Attempt One
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:
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.
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.
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
Note
When writing the decision procedure for littleMissDirect you will
want to first define the procedure signature for allTrueBravo first.
and then realise littleMissDirect.
and then give the procedure body for allTrueBravos.
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.