> Isn't it a bit odd that the type signature "contains" the uncompressed data? There would seem to be no point in compressing data this way. I agree it's a bit

> Isn't it a bit odd that the type signature "contains" the uncompressed data? There would seem to be no point in compressing data this way. I agree it's a bit tricky to understand (which is why I don't like that representation), but this has nothing to do with laziness (Idris is a strict language). It's a more general phenomenon that values in a type signature do not actually have to exist at runtime. It's purely a notational thing that lives in the type-checkers "brain" and has no runtime representation. At runtime, `compress` really does compress the list without keeping a copy of it anywhere. For any type `MyType someValue`, there's no a priori reason `someValue` should actually have any runtime representation. See e.g. data MyType : Int -> Type TheOnlyThingOfMyType : MyType 5 -- There's no way to actually access the 5 at runtime -- It only lives in type signatures someValue : MyType 5 someValue = TheOnlyThingOfMyType -- This addition takes place at compile time, not runtime someOtherValue : MyType (4 + 1) someOtherValue = TheOnlyThingOfMyType thisFailsToCompile : MyType (4 + 2) thisFailsToCompile = TheOnlyThingOfMyType There is likewise no reason to believe something like `SomeOtherType String` actually has a string in it anywhere (this pattern is known as a phantom type) without knowing more about `SomeOtherType`. All the type parameter does is constrain how functions can be called that involve the overall type. In this sense `List String` having an actual `String` you can pull out of it at runtime can be thought of as the exception rather than the norm (and indeed isn't always the case, e.g. if you have an empty list). In this case, you can use `RunLength`'s list parameter to state more invariants, even if the list doesn't exist at runtime. -- If two lists compress to the same thing, then they must've been the same to begin with compressionIsLossless : RunLength xs = RunLength ys -> xs = ys -- Here follows the proof of that statement -- If the proof looks confusing, https://shuangrimu.com/posts/language-agnostic-intro-to-dependent-types.html might help compressionIsLossless runLengthsAreEqual = case runLengthsAreEqual of Refl => Refl Switching back to my representation... > But couldn't do that by having a single compress function and proving that it works? Why have more than one? I only have one compress function (I was just too lazy to write it out and used ellipses instead). > Proving that all run-length encodings decompress to some list doesn't seem interesting? This is just as true of your encoding. The constraint is fairly simple, but very strong (although I made a typo where the name associated with the type signature and the actual implementation's name are different, d'oh): uncompressIsTheInverseOfCompress : uncompress(compress xs) = xs uncompressIsTheInverseOfCompress = ... -- Too lazy to write out the actual proof at the moment This is the fundamental property all lossless compression schemes must satisfy. You could also of course add all sorts of other properties. -- Even though it won't inflate list length, it can result in more memory usage due to the tuples compressWontInflateSize : (length (compress xs) <= length xs) = True compressWontInflateSize = ... -- Again too lazy to write out the proof -- Idris doesn't have a general exists statement so we need to provide a -- concrete example compressMakesAtLeastOneListSmaller : (length (compress [1, 1, 1]) <= length [1, 1, 1])) = True compressMakesAtLeastOneListSmaller = Refl -- This proof is easy, just tell Idris to actually do the calculation (at compile-time, not run-time!) > Apparently type-checking proofs aren't really about concretely showing that data is consistent? If you rely on the proof, you assume correct data rather than verifying it. A sufficiently smart compiler might optimize away your attempted verification? I'm not sure what you mean here. In order to show that your data is consistent you need to describe what you mean by consistency somehow. You can do that either within the definition of a type itself (which I do not like) or you can do that by explaining how different functions are supposed to relate to each other (e.g. how compress, uncompress, and length should be related to each other), which I like more. As for "optimizing away verification," that's the point of Idris' 0 multiplicity. It marks something as "compile-time-only" that has no runtime representation and hence no runtime performance impact.