Data.List.Fresh

Agda で昨日発見しました。sort された List を宣言できるという超素晴らしい。

　　ins : ISortedList
　　ins = 0 ∷# 1 ∷# 3 ∷# 10 ∷# []

いや、なにが素晴らしいか全然伝わらないと思うんですが、順序を間違えるとエラーになる。

いや、そこじゃなくて「順序が正しいことを実行や証明で使える」ってところ。

ところが、

　　module _ {a} (A : Set a) (R : Rel A r) where
　　　data List# : Set (a ⊔ r)
　　　fresh : (a : A) (as : List#) → Set r
　　　data List# where
　　　　[]　 : List#
　　　　cons : (a : A) (as : List#) → fresh a as → List#
　　　infixr 5 _∷#_
　　　pattern _∷#_ x xs = cons x xs _
　　　fresh a []　　　　= ⊤
　　　fresh a (x ∷# xs) = R a x × fresh a xs

簡単な定義のわりにさっぱりわからない。fresh ってなんだ? いや、

　　単に insert したいだけなんですが...

で、見つけたのがここ。なるほど、total つまり、≦ か ≧ どっちかってのを使うのか。そもそも

　　　fresh : (a : A) (as : List#) → Set r

Set を返す関数ってのは普通のプログラミングには出てこないし、単なる型とも違うので難しい。

　 ttf : (a : FL (suc n)) → (y : FList {suc n}) →　fresh (FL (suc n)) ⌊ _f<?_ ⌋　a y　→ fresh (FL (suc n)) ⌊ _f<?_ ⌋　x y
　 ttf a [] fr = Level.lift tt

こんな風に、関数で定義された型で受けるらしいです。いや、Agda、まだまだ、新鮮だな。

https://gist.github.com/aristidb/1684202