Search code examples
haskelldependent-type

Monotonic sequence type in haskell

I would like to define a type for infinite number sequence in haskell. My idea is:

type MySeq = Natural -> Ratio Integer

However, I would also like to be able to define some properties of the sequence on the type level. A simple example would be a non-decreasing sequence like this. Is this possible to do this with current dependent-type capabilities of GHC?

EDIT: I came up with the following idea:

type PositiveSeq = Natural -> Ratio Natural
data IncreasingSeq = IncreasingSeq {
  start :: Ratio Natural,
  diff :: PositiveSeq}

type IKnowItsIncreasing = [Ratio Natural]

getSeq :: IncreasingSeq -> IKnowItsIncreasing
getSeq s = scanl (+) (start s) [diff s i | i <- [1..]]

Of course, it's basically a hack and not actually type safe at all.

Solution

  • This isn't doing anything very fancy with types, but you could change how you interpret a sequence of naturals to get essentially the same guarantee.

    I think you are thinking along the right lines in your edit to the question. Consider

    data IncreasingSeq = IncreasingSeq (Integer -> Ratio Natural)

    where each ratio represents how much it has increased from the previous number (starting with 0).

    Then you can provide a single function

    applyToIncreasing :: ([Ratio Natural] -> r) -> IncreasingSeq -> r
applyToIncreasing f (IncreasingSeq s) = f . drop 1 $ scanl (+) 0 (map (s $) [0..])

    This should let you deconstruct it in any way, without allowing the function to inspect the real structure.

    You just need a way to construct it: probably a fromList that just sorts it and an insert that performs a standard ordered insertion.

    It pains part of me to say this, but I don't think you'd gain anything over this using fancy type tricks: there are only three functions that could ever possibly go wrong, and they are fairly simple to correctly implement. The implementation is hidden so anything that uses those is correct as a result of those functions being correct. Just don't export the data constructor for IncreasingSeq.

    I would also suggest considering making [Ratio Natural] be the underlying representation. It simplifies things and guarantees that there are no "gaps" in the sequence (so it is guaranteed to be a sequence).

    If you want more safety and can take the performance hit, you can use data Nat = Z | S Nat instead of Natural.

    I will say that if this was Coq, or a similar language, instead of Haskell I would be more likely to suggest doing some fancier type-level stuff (depending on what you are trying to accomplish) for a couple reasons:

    1. In systems like Coq, you are usually proving theorems about the code. Because of this, it can be useful to have a type-level proof that a certain property holds. Since Haskell doesn't really have a builtin way to prove those sorts of theorems, the utility diminishes.

    2. On the other hand, we can (sometimes) construct data types that essentially must have the properties we want using a small number of trusted functions and a hidden implementation. In the context of a system with more theorem proving capability, like Coq, this might be harder to convince theorem prover of the property than if we used a dependent type (possibly, at least). In Haskell, however, we don't have that issue in the first place.