0 | ||| This module implements a relation between a natural number and a list.
  1 | ||| The relation witnesses the fact the number is the length of the list.
  2 | |||
  3 | ||| It is meant to be used in a runtime-irrelevant fashion in computations
  4 | ||| manipulating data indexed over lists where the computation actually only
  5 | ||| depends on the length of said lists.
  6 | |||
  7 | ||| Instead of writing:
  8 | ||| ```idris example
  9 | ||| f0 : (xs : List a) -> P xs
 10 | ||| ```
 11 | |||
 12 | ||| We would write either of:
 13 | ||| ```idris example
 14 | ||| f1 : (n : Nat) -> (0 _ : HasLength n xs) -> P xs
 15 | ||| f2 : (n : Subset n (flip HasLength xs)) -> P xs
 16 | ||| ```
 17 | |||
 18 | ||| See `sucR` for an example where the update to the runtime-relevant Nat is O(1)
 19 | ||| but the update to the list (were we to keep it around) an O(n) traversal.
 20 |
 21 | module Data.List.HasLength
 22 |
 23 | import Data.DPair
 24 | import Data.List
 25 | import Data.Nat
 26 |
 27 | %default total
 28 |
 29 | ------------------------------------------------------------------------
 30 | -- Type
 31 |
 32 | ||| Ensure that the list's length is the provided natural number
 33 | public export
 34 | data HasLength : Nat -> List a -> Type where
 35 |   Z : HasLength Z []
 36 |   S : HasLength n xs -> HasLength (S n) (x :: xs)
 37 |
 38 | ||| This specification corresponds to the length function
 39 | export
 40 | hasLength : (xs : List a) -> HasLength (length xs) xs
 41 | hasLength [] = Z
 42 | hasLength (_ :: xs) = S (hasLength xs)
 43 |
 44 | export
 45 | take : (n : Nat) -> (xs : Stream a) -> HasLength n (take n xs)
 46 | take Z _ = Z
 47 | take (S n) (x :: xs) = S (take n xs)
 48 |
 49 | ------------------------------------------------------------------------
 50 | -- Properties
 51 |
 52 | ||| The length is unique
 53 | export
 54 | hasLengthUnique : HasLength m xs -> HasLength n xs -> m === n
 55 | hasLengthUnique Z Z = Refl
 56 | hasLengthUnique (S p) (S q) = cong S (hasLengthUnique p q)
 57 |
 58 | export
 59 | hasLengthAppend : HasLength m xs -> HasLength n ys -> HasLength (m + n) (xs ++ ys)
 60 | hasLengthAppend Z ys = ys
 61 | hasLengthAppend (S xs) ys = S (hasLengthAppend xs ys)
 62 |
 63 | hasLengthReverseOnto : HasLength m acc -> HasLength n xs -> HasLength (m + n) (reverseOnto acc xs)
 64 | hasLengthReverseOnto p Z = rewrite plusZeroRightNeutral m in p
 65 | hasLengthReverseOnto {n = S n} p (S q) = rewrite sym (plusSuccRightSucc m n) in hasLengthReverseOnto (S p) q
 66 |
 67 | export
 68 | hasLengthReverse : HasLength m acc -> HasLength m (reverse acc)
 69 | hasLengthReverse = hasLengthReverseOnto Z
 70 |
 71 | export
 72 | map : (f : a -> b) -> HasLength n xs -> HasLength n (map f xs)
 73 | map f Z = Z
 74 | map f (S n) = S (map f n)
 75 |
 76 | ||| @sucR demonstrates that snoc only increases the length by one
 77 | ||| So performing this operation while carrying the list around would cost O(n)
 78 | ||| but relying on n together with an erased HasLength proof instead is O(1)
 79 | export
 80 | sucR : HasLength n xs -> HasLength (S n) (snoc xs x)
 81 | sucR Z = S Z
 82 | sucR (S n) = S (sucR n)
 83 |
 84 | ------------------------------------------------------------------------
 85 | -- Views
 86 |
 87 | namespace SubsetView
 88 |
 89 |   ||| We provide this view as a convenient way to perform nested pattern-matching
 90 |   ||| on values of type `Subset Nat (flip HasLength xs)`. Functions using this view will
 91 |   ||| be seen as terminating as long as the index list `xs` is left untouched.
 92 |   ||| See e.g. listTerminating below for such a function.
 93 |   public export
 94 |   data View : (xs : List a) -> Subset Nat (flip HasLength xs) -> Type where
 95 |     Z : View [] (Element Z Z)
 96 |     S : (p : Subset Nat (flip HasLength xs)) -> View (x :: xs) (Element (S (fst p)) (S (snd p)))
 97 |
 98 |   ||| This auxiliary function gets around the limitation of the check ensuring that
 99 |   ||| we do not match on runtime-irrelevant data to produce runtime-relevant data.
100 |   viewZ : (0 p : HasLength Z xs) -> View xs (Element Z p)
101 |   viewZ Z = Z
102 |
103 |   ||| This auxiliary function gets around the limitation of the check ensuring that
104 |   ||| we do not match on runtime-irrelevant data to produce runtime-relevant data.
105 |   viewS : (n : Nat) -> (0 p : HasLength (S n) xs) -> View xs (Element (S n) p)
106 |   viewS n (S p) = S (Element n p)
107 |
108 |   ||| Proof that the view covers all possible cases.
109 |   export
110 |   view : (p : Subset Nat (flip HasLength xs)) -> View xs p
111 |   view (Element Z p) = viewZ p
112 |   view (Element (S n) p) = viewS n p
113 |
114 | namespace CurriedView
115 |
116 |   ||| We provide this view as a convenient way to perform nested pattern-matching
117 |   ||| on pairs of values of type `n : Nat` and `HasLength xs n`. If transformations
118 |   ||| to the list between recursive calls (e.g. mapping over the list) that prevent
119 |   ||| it from being a valid termination metric, it is best to take the Nat argument
120 |   ||| separately from the HasLength proof and the Subset view is not as useful anymore.
121 |   ||| See e.g. natTerminating below for (a contrived example of) such a function.
122 |   public export
123 |   data View : (xs : List a) -> (n : Nat) -> HasLength n xs -> Type where
124 |     Z : View [] Z Z
125 |     S : (n : Nat) -> (0 p : HasLength n xs) -> View (x :: xs) (S n) (S p)
126 |
127 |   ||| Proof that the view covers all possible cases.
128 |   export
129 |   view : (n : Nat) -> (0 p : HasLength n xs) -> View xs n p
130 |   view Z Z = Z
131 |   view (S n) (S p) = S n p
132 |
133 | ------------------------------------------------------------------------
134 | -- Examples
135 |
136 | -- /!\ Do NOT re-export these examples
137 |
138 | listTerminating : (p : Subset Nat (flip HasLength xs)) -> HasLength (S (fst p)) (xs ++ [x])
139 | listTerminating p with (view p)
140 |   listTerminating (Element 0 Z) | Z = S Z
141 |   listTerminating (Element (S (fst y)) (S (snd y))) | (S y) = S (listTerminating y)
142 |
143 | data P : List Nat -> Type where
144 |   PNil : P []
145 |   PCon : P (map f xs) -> P (x :: xs)
146 |
147 | covering
148 | notListTerminating : (p : Subset Nat (flip HasLength xs)) -> P xs
149 | notListTerminating p with (view p)
150 |   notListTerminating (Element 0 Z) | Z = PNil
151 |   notListTerminating (Element (S (fst y)) (S (snd y))) | (S y) =
152 |     PCon (notListTerminating {xs = map id (tail xs)} ({ snd $= map id } y))
153 |
154 | natTerminating : (n : Nat) -> (0 p : HasLength n xs ) -> P xs
155 | natTerminating n p = case view n p of
156 |   Z => PNil
157 |   S n p => PCon (natTerminating n (map id p))
158 |
159 |