A sibling comment correctly lays out what the type means, and I'll elaborate a little more here. > how the data is stored Thinking of how concretely the data

A sibling comment correctly lays out what the type means, and I'll elaborate a little more here. > how the data is stored Thinking of how concretely the data is stored is a little bit tricky. I find it easier to build an intuition by looking at what kind of values the type signature lets us build, and which values are disallowed. runLengthOfAnEmptyList : RunLength [] runLengthOfAnEmptyList = Empty -- Note that 1 is shorthand for (S Z) runLengthOfAListWithOneElement : RunLength [ 1 ] runLengthOfAListWithOneElement = Run 0 1 Empty -- The definition of RunLength places restrictions on how to -- construct it. -- For example, this will not compile. runLengthOfAListWithOneElementBrokenVersion : RunLength [ 1 ] runLengthOfAListWithOneElementBrokenVersion = Run 1 1 Empty -- -- This violates the type signature of RunLength -- Notice Run 1 1 Empty which has changed the 0 to a 1 -- -- As a reminder this is the definition of Run -- Run : ( n : Nat ) -> ( x : ty ) -> ( rle : RunLength more ) -> -- RunLength ( rep ( S n ) x ++ more ) -- -- n is set to 1, x is set to 1, and Empty means that more is set to [] -- Making the necessary substitutions results in: -- RunLength ( rep ( S n ) x ++ more ) -- No substitutions yet -- RunLength ( rep ( S 1 ) 1 ++ [] ) -- S 1 is the same thing as S (S Z) -- RunLength ( 1 :: 1 :: [] ++ [] ) -- Substituting rep ( S 1 ) 1 -- RunLength ( 1 :: 1 :: [] ) -- ++ [] doesn't change our list at all -- RunLength [ 1, 1 ] -- Syntax sugar for 1 :: 1 :: [] -- -- But this is a contradiction! Since we said in our type annotation that we -- should have RunLength [ 1 ], not RunLength [ 1, 1 ]! However I agree with you that this style of dependently typed programming is confusing and ultimately in my view, a bad representation of how dependent types should be used in production code (if any full-spectrum dependently typed language gains enough adoption to be used in large production projects). Here's the same idea in an alternative, but (roughly) equivalent, encoding, which hopefully lays it out more clearly. RuntimeEncodedList : Type -> Type RuntimeEncodedList t = List (Nat, t) uncompress : RuntimeEncodedList t -> List t uncompress runtimeEncodedList = case runtimeEncodedList of [] => [] (n, elem) :: restOfList => rep (n + 1) elem ++ uncompress restOfList compress : List t -> RuntimeEncodedList t compress = ... uncompressIsTheInverseOfCompress : uncompress (compress xs) = xs uncompressCorrectlyUncompressesEmptyLists = ... I hope this is a much plainer and easier to understand representation, with a similarly strong invariant. The `...` are of course eliding a lot, but my point is that they can be elided, without really affecting comprehension of the overall code (which is not the case with the other representation). This also nicely avoids a problem I see in a lot of dependently code where the structural representation of data structures are intertwined with the invariants they are supposed to uphold. Not only does this result in increasingly confusing code as the invariants get more sophisticated and also awkwardly privileges certain invariants over others, it makes modifying the representation in even the smallest ways a nightmarish test of resolve. This is because everywhere you want to create the data structure, you must also prove that the invariants hold. Sometimes this proof is trivial, sometimes this proof is difficult. But you must always do this, you cannot bail out with some sort of "believe me" escape hatch where you maybe use some sort of external solver to prove it instead, because you can now potentially crash or even segfault your program, even if your code would otherwise fulfill the invariant through some other reasoning the compiler cannot see, since the proof is an integral part of the runtime representation of the data structure. This sort of proof burden means that it can be a Herculean task to swap out the underlying representation of the data structure for a more efficient one (e.g. you're going to be in for a hard time if you've written code with the `RunLength` type and all of a sudden, for speed reasons, you'd prefer an underlying representation of run length encoded types that groups all the run lengths in one array and stores all the actual values in another array). At least having zero multiplicity annotations on parts of the dependently typed data structure makes things a bit easier. I instead advocate for a clean separation where the overwhelming majority of data types in a dependently-typed program should be non-dependently-typed and dependent types used instead merely to state properties about those data types independently.