1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
------------------------------------------------------------------------
-- The Agda standard library
--
-- Example use case for a fresh list: sorted list
------------------------------------------------------------------------
{-# OPTIONS --sized-types #-}
module README.Data.List.Fresh where
open import Data.Nat
open import Data.List.Base
open import Data.List.Fresh
open import Data.List.Relation.Unary.AllPairs as AllPairs using (AllPairs)
open import Data.Product.Base using (_,_; proj₁; proj₂)
open import Relation.Nary using (⌊_⌋; fromWitness)
-- A sorted list of natural numbers can be seen as a fresh list
-- where the notion of freshness is being smaller than all the
-- existing entries
SortedList : Set
SortedList = List# ℕ _<_
_ : SortedList
_ = cons 0 (cons 1 (cons 3 (cons 10 [] _)
(s≤s (s≤s (s≤s (s≤s z≤n))) , _))
(s≤s (s≤s z≤n) , s≤s (s≤s z≤n) , _))
(s≤s z≤n , s≤s z≤n , s≤s z≤n , _)
-- Clearly, writing these by hand can pretty quickly become quite cumbersome
-- Luckily, if the notion of freshness we are using is decidable, we can
-- make most of the proofs inferrable by using the erasure of the relation
-- rather than the relation itself!
-- We call this new type *I*SortedList because all the proofs will be implicit.
ISortedList : Set
ISortedList = List# ℕ ⌊ _<?_ ⌋
-- The same example is now much shorter. It looks pretty much like a normal list
-- except that we know for sure that it is well ordered.
ins : ISortedList
ins = 0 ∷# 1 ∷# 3 ∷# 10 ∷# []
-- Indeed we can extract the support list together with a proof that it
-- is ordered thanks to the combined action of toList converting a fresh
-- list to a pair of a list and a proof and fromWitness which "unerases"
-- a proof.
ns : List ℕ
ns = proj₁ (toList ins)
sorted : AllPairs _<_ ns
sorted = AllPairs.map (fromWitness _<_ _<?_) (proj₂ (toList ins))
-- See the following module for an applied use-case of fresh lists
open import README.Data.Trie.NonDependent
|
