I’ve many times heard the following:

A dependent type is a type whose definition depends on a value.

Sounds simple, but I’ve never actually been able to imagine what that means in practice. It didn’t help that what is usually shown is what I now know to be “dependent function types” (Π type) rather than the much simpler “dependent pair type” (Σ type).

Now what does that actually mean?

Ada (Σ type)🔗

There is a quote mentioned in the post On Ada’s Dependent Types, and its Types as a Whole:

It’s tons of extremely complex functional languages, formal theorem provers, and… Ada, a random Government Language dating back to 1983.

In Ada composite types can have so-called “Discriminants”. These are both parts of the type itself and its value.

If a given type has discriminants then the type itself is more of a large family of types, where each assignment of values to the discriminants is a concrete type.

If we wanted to construct a maybe type, it could be done like so:

type Maybe(Has_Value : Boolean) is
   record

      case Has_Value is
         when True =>
            Value : Integer;
         when False =>
            null;
      end case;

   end record;

Now if we use it:

V1 : Maybe(Has_Value => True)  := (Has_Value => True, Value => 20);
V2 : Maybe(Has_Value => False) := (Has_Value => False);

These are both correct, the Has_Value specified as part of the type constrains the record to have that value in its Has_Value field, and Value only exists if Has_Value is true.

Assigning a conflicting record will yield an warning¹:

V3 : Maybe(Has_Value => False) := (Has_Value => True, Value => 30);

   V3 : Maybe(Has_Value => False) := (Has_Value => True, Value => 30);
                                     |
>>> warning: incorrect value for discriminant "Has_Value" [enabled by default]
>>> warning: Constraint_Error will be raised at run time [enabled by default]

And we get a hard error if we try to initialize or fail to initialize the value when it isn’t or is present respectively:

V4 : Maybe(Has_Value => False) := (Has_Value => False, Value => 30);
V5 : Maybe(Has_Value => True)  := (Has_Value => True);

   V4 : Maybe(Has_Value => False) := (Has_Value => False, Value => 30);
                                                          |
>>> error: "Value" is not a component of the aggregate subtype

   V5 : Maybe(Has_Value => True)  := (Has_Value => True);
                                     |
>>> error: no value supplied for component "value"

The reason the discriminant is written separately like this, is to separate the fields that are part of the type and can thus be used to define its fields, and those that can’t.

There are some limitations for the discriminants, for example they have to have a known layout, if you don’t know where to look for the thing that defines the type or what it looks like, you can’t really tell what it is. Which is why you have to parameterize a Vector for example with a known maximum range, otherwise you wouldn’t be able to know where the range definition ends without extra information (of course you can nest records for that purpose).

It is acceptable to access parts of the record you know are there even if some of the discriminants are not known yet, which complicates this slightly, but the idea stays the same.

If we look at the theory², we see that this is beautifully described as a “dependent pair”. Imagine a tuple, where the left value is given, but the right value’s type is a function from the left value to a type.

The above would be something like (a :: Bool, b :: Bool -> Subtype_of_Maybe). The b value is just a value, it’s just the type that needs an input of the value of a to determine what is actually in there. What’s in there was decided beforehand by someone constructing the tuple, and the type gives you enough information to determine what type and layout b has, but you first have to inspect a to determine that yourself.

The following is completely valid:

V6 : Maybe := (Has_Value => True,
               Value => 30);

You just have to inspect a (the discriminant) to figure out what the record’s actual layout is before you can access it.

There is a pattern I’ve seen, where the struct partly or entirely depends on an enum type, which the Ada folk seem to usually name “Kind”³.

Something like:

type Either_Kind is (Left, Right);

type Either(Kind : Either_Kind) is
   record

      case Kind is
         when Left =>
            Left : Integer;
         when Right =>
            Right : Character;
      end case;

   end record;

Seem familiar? This is just a regular sum type (discriminated union). Sum types are just dependent pairs where the first item is a fully matched enum.

Idris (Π type)🔗

This is a very similar concept, with the main distinction that the type that’s depending on a value need not be associated in one composite value.

What worked as an intuition for me is that it’s a dependent pair which is scattered about the program, the wait they are connected is by passing through a function that takes the dependee and returns a dependent. Then inspecting the dependee’s value allows us to determine the type of the dependent.

As can be seen in this IntOrString example from the Idris example page:

module Main

IntOrString : (a : Bool) -> Type
IntOrString True = Int
IntOrString False = String

foo : (a : Bool) -> (IntOrString a)
foo True = 0
foo False = "0"

main : IO ()
main = let
        x = True
        y = foo x
       in
         if x
         then print (y : Int)
         else print (y : String)

The if here discriminates the two cases of IntOrString allowing us to use it as the concrete type.

Footnotes🔗

¹ This will fail at runtime in Ada or at compile-time with SPARK verification.

² Forgive my source being the Wiki for this

³ Even though it’s literally not a Kind but a type.