How can I get the length of dependently typed interval?

Question

Say I have a data type

data Interval :: Nat -> Nat -> * where
  Go :: Interval m n -> Interval m (S n)
  Empty :: SNat n -> Interval n n

These are half-(right-)open intervals. Nat are the standard inductive naturals, SNat are the corresponding singletons.

Now I'd like to get a singleton Nat for the length of a given interval:

intervalLength :: Interval n (Plus len n) -> SNat len
intervalLength Empty = Z
intervalLength (Go i) = S (intervalLength i)

This does not work, as the Plus function is not injective. I could probably define it like

intervalLength :: Interval m n -> SNat (Minus n m)

but that would require some lemmas (and additional constraints), I guess. Also, my intervals arise in the former shape.

Background: I tried to do this in Omega and it did not work (omega bug I filed)

Also how could these problems be cracked with modified typecheckers? Can the RHS of the supply the crucial hint to LHS pattern's type equation so that the non-injectiveness cancels out?

How do Agda programmers tackle these problems?

Answer 1

Here's my version of your program. I'm using

{-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies #-}

and I've got Nat and its singleton

data Nat = Z | S Nat

data SNat :: Nat -> * where
  ZZ :: SNat Z
  SS :: SNat n -> SNat (S n)

Your Interval type is more familiar to me as the "suffix" definition of "less-than-or-equal": "suffix" because if you upgraded from numbers to lists and labelled each S with an element, you'd have the definition of a list suffix.

data Le :: Nat -> Nat -> * where
  Len :: SNat n -> Le n n
  Les :: Le m n -> Le m (S n)

Here's addition.

type family Plus (x :: Nat) (y :: Nat) :: Nat
type instance Plus Z     y  = y
type instance Plus (S x) y  = S (Plus x y)

Now, your puzzle is to count the Les constructors in some Le-value, extracting the singleton for the difference between its indices. Rather than assuming that we're working with some Le n (Plus m n) and trying to compute a SNat m, I'm going to write a function which computes the difference between arbitrary Le m o-indices and establishes the connection with Plus.

Here's the additive definition of Le, with singletons supplied.

data AddOn :: Nat -> Nat -> * where
  AddOn :: SNat n -> SNat m -> AddOn n (Plus m n)

We can easily establish that Le implies AddOn. Pattern matching on some AddOn n o reveals o to be Plus m n for some m and hands us the singletons we wanted.

leAddOn :: Le m o -> AddOn m o
leAddOn (Len n) = AddOn n ZZ
leAddOn (Les p) = case leAddOn p of AddOn n m -> AddOn n (SS m)

More generally, I'd advise formulating dependently typed programming problems minimizing the presence of defined functions in the indices of types over which you plan to match. This avoids complicated unification. (Epigram used to colour such functions green, hence the advice "Don't touch the green slime!".) Le n o, it turns out (for that is the point of leAddOn), is no less informative a type than Le n (Plus m n), but it is rather easier to match on.

Yet more generally, it is quite a normal experience to set up a dependent datatype which captures the logic of your problem but is absolutely ghastly to work with. This does not mean that all datatypes which capture the correct logic will be absolutely ghastly to work with, just that you need think harder about the ergonomics of your definition. Getting these definitions neat is not a skill that very many people pick up in their ordinary Functional Programming learning experience, so expect to climb a new learning curve.

Answer 2

I had a go at this in Idris. While I agree with pigworker's suggestion of reformulating the problem, here's what you'd have to do to get your definition past the Idris type checker. First, the singleton Nats:

data SNat : Nat -> Set where
   ZZ : SNat O
   SS : SNat k -> SNat (S k)

Then, the definition of intervals:

data Interval : Nat -> Nat -> Set where
  Go : Interval m n -> Interval m (S n)
  Empty : SNat n -> Interval n n

The definition you want for intervalLength looks a bit like this:

intervalLength : Interval n (plus len n) -> SNat len
intervalLength (Empty sn) = ZZ
intervalLength (Go i)     = SS (intervalLength i)

But you'll run into trouble, because as you say plus is not injective. We can get somewhere by additionally pattern matching on len explicitly - then unification can make some progress:

intervalLength : Interval n (plus len n) -> SNat len
intervalLength {len = O}   (Empty sn) = ZZ
intervalLength {len = S k} (Go i)     = SS (intervalLength i)

This is fine, and gets past the typechecker, but unfortunately it doesn't believe that the function is total:

*interval> :total intervalLength
not total as there are missing cases

The missing case is this one:

intervalLength {len = O}   (Go i)     = ?missing

If you try this, and ask the REPL for the type of missing, you'll see:

missing : (n : Nat) -> (i : Interval (S n) n) -> SNat O

Now, we know that the type Interval (S n) n is empty, but alas, the type checker does not. Somehow we need to write badInterval : Interval (S n) n -> _|_, then we can say:

intervalLength {len = O}   (Go i)     = FalseElim (badInterval i)

I will leave the definition of badInterval as an exercise :-). It's not especially tricky, but it is a bit boring to have to do - sometimes it's hard to avoid having to work with types of this sort, but implementing badInterval backs up pigworker's suggestion of not doing it this way!