mirror of
https://github.com/GrammaticalFramework/gf-core.git
synced 2026-04-13 23:09:31 -06:00
37 lines
1.0 KiB
Plaintext
37 lines
1.0 KiB
Plaintext
Monoid : Type -> Type
|
|
Monoid A = sig { zero : A; plus : A -> A -> A }
|
|
|
|
Additive : Type -> Type
|
|
Additive = Monoid
|
|
|
|
additive_Integer : Additive Integer
|
|
additive_Integer = rec { zero = 0; plus = prim_add_Int }
|
|
|
|
sum : (A:Type) -> Additive A -> List A -> A
|
|
sum _ d (Nil _) = d.zero
|
|
sum A d (Cons _ x xs) = d.plus x (sum A d xs)
|
|
|
|
|
|
|
|
|
|
Show : Type -> Type
|
|
Show A = sig { show : A -> String }
|
|
|
|
show : (A : Type) -> Show A -> A -> String
|
|
show _ rec{show = show} x = show x
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Compos : (C : Type) -> (C -> Type) -> Type
|
|
Compos C T = sig
|
|
composOp : (c : C) -> ((d : C) -> T d -> T d) -> T c -> T c
|
|
composFold : (B : Type) -> Monoid B -> (c : C) -> ((d : C) -> T d -> b) -> T c -> b
|
|
|
|
composOp : (T : Type) -> (C : Type) -> Compos C T -> (c : C) -> ((d : C) -> T d -> T d) -> T c -> T c
|
|
composOp _ _ rec{composOp=composOp} c f t = composOp c f t
|
|
|
|
composFold : (T : Type) -> (C : Type) -> Compos C T -> (B : Type) -> Monoid B -> ((d : C) -> T d -> b) -> T c -> b
|
|
composFold _ _ rec{composFold=composFold} b m c f t = composFold b m c f t |