quox/examples/list.quox

89 lines
2.1 KiB
Text
Raw Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

def0 Vec : 0. → 0.★₀ → ★₀ =
λ n A ⇒
caseω n return ★₀ of {
zero ⇒ {nil};
succ _, 0.Tail ⇒ A × Tail
};
def0 List : 0.★₀ → ★₀ =
λ A ⇒ (len : ) × Vec len A;
defω nil : 0.(A : ★₀) → List A =
λ A ⇒ (0, 'nil);
defω S : 1. = λ n ⇒ succ n;
defω cons : 0.(A : ★₀) → 1.A → 1.(List A) → List A =
λ A x xs ⇒
case1 xs return List A of {
(len, elems) ⇒ (succ len, x, elems)
};
{-
-- needs coercions overall,
-- and real w-types to be linear
defω list-ind :
0.(A : ★₀) →
0.(P : ω.(List A) → ★₀) →
1.(n : P (nil A)) →
ω.(c : 1.(x : A) → 0.(xs : List A) → 1.(P xs) → P (cons A x xs)) →
1.(lst : List A) → P lst =
λ A P n c lst ⇒
case1 lst return l ⇒ P l of {
(len, elems) ⇒
case1 len return len' ⇒ P (len', elems) of {
zero ⇒ n;
succ len', 1.ih ⇒
case1 elems return P (succ len', elems) of {
(first, rest) ⇒ c first rest ih
}
}
};
defω foldr :
0.(A : ★₀) → 0.(B : ★₀) →
1.(n : B) → ω.(c : 1.A → 1.B → B) →
1.(List A) → B =
λ A B n c lst ⇒ list-ind A (λ _ ⇒ B) n (λ a as b ⇒ c a b) lst;
-- ...still does
defω foldr :
0.(A : ★₀) → 0.(B : ★₀) →
ω.(n : B) → ω.(c : 1.A → 1.B → B) →
ω.(List A) → B =
λ A B n c lst ⇒
caseω lst return B of {
(len, elems) ⇒
caseω len return B of {
zero ⇒ caseω elems return B of { 'nil ⇒ n };
succ _, ω.ih ⇒
caseω elems return B of {
(first, rest) ⇒ c first ih
}
}
};
-}
defω plus : 1. → 1. =
λ m n ⇒
case1 m return of {
zero ⇒ n;
succ _, 1.mn ⇒ succ mn
};
-- case-'s qout needs to be Σz + ωΣs
def0 plus-3-3 : plus 3 3 ≡ 6 : =
δ 𝑖 ⇒ 6;
{-
defω sum : ω.(List ) → = foldr 0 plus;
defω numbers : List =
(5, (0, 1, 2, 3, 4, 'nil));
defω number-sum : sum numbers ≡ 10 : =
δ _ ⇒ 10;
-}