diff --git a/transfer/examples/overload.tr b/transfer/examples/overload.tr index 32d617d28..09d62d15f 100644 --- a/transfer/examples/overload.tr +++ b/transfer/examples/overload.tr @@ -1,29 +1,148 @@ -Monoid : Type -> Type -Monoid A = sig { zero : A; plus : A -> A -> A } +-- +-- The Add class +-- -Additive : Type -> Type -Additive = Monoid +-- FIXME: reimplement in terms of Monoid? -additive_Integer : Additive Integer -additive_Integer = rec { zero = 0; plus = prim_add_Int } +Add : Type -> Type +Add = sig { zero : A; plus : A -> A -> A } -sum : (A:Type) -> Additive A -> List A -> A +zero : (A : Type) -> Add A -> A +zero _ d = d.zero + +plus : (A : Type) -> Add A -> A -> A -> A +plus _ d = d.plus + +add_Integer : Add Integer +add_Integer = rec { zero = 0; plus = prim_add_Int } + +sum : (A:Type) -> Add A -> List A -> A sum _ d (Nil _) = d.zero sum A d (Cons _ x xs) = d.plus x (sum A d xs) +{- Operators: + + (x + y) => (plus ? ? x y) + +-} + +-- +-- The Prod class +-- + +-- FIXME: reimplement in terms of Monoid? + +Prod : Type -> Type +Prod = sig { one : A; times : A -> A -> A } + +one : (A : Type) -> Prod A -> A +one _ d = d.zero + +times : (A : Type) -> Prod A -> A -> A -> A +times _ d = d.plus + +prod_Integer : Add Integer +prod_Integer = rec { one = 1; times = prim_mul_Int } + +product : (A:Type) -> Prod A -> List A -> A +product _ d (Nil _) = d.one +product A d (Cons _ x xs) = d.times x (product A d xs) + +{- Operators: + + (x * y) => (times ? ? x y) + +-} +-- +-- The Eq class +-- + +Eq : Type -> Type +Eq A = sig { eq : A -> A -> Bool } + +eq : (A : Type) -> Eq A -> A -> A -> Bool +eq _ d = d.eq + +neq : (A : Type) -> Eq A -> A -> A -> Bool +neq A d x y = not (eq A d x y) + + +{- Operators: + + (x == y) => (eq ? ? x y) + (x /= y) => (neq ? ? x y) + +-} + + +-- +-- The Ord class +-- + +-- FIXME: require Eq for Ord + +data Ordering : Type where + LT : Ordering + EQ : Ordering + GT : Ordering + +Ord : Type -> Type +Ord A = sig { compare : A -> A -> Ordering } + +compare : (A : Type) -> Ord A -> A -> A -> Ordering +compare _ d = compare + +ordOp : (Ordering -> Bool) -> (A : Type) -> Ord A -> A -> A -> Bool +ordOp f A d x y = f (compare A d x y) + +lt : (A : Type) -> Ord A -> A -> A -> Bool +lt = ordOp (\o -> case o of { LT -> True; _ -> False }) + +le : (A : Type) -> Ord A -> A -> A -> Bool +le = ordOp (\o -> case o of { GT -> False; _ -> True }) + +ge : (A : Type) -> Ord A -> A -> A -> Bool +ge = ordOp (\o -> case o of { LT -> False; _ -> True }) + +gt : (A : Type) -> Ord A -> A -> A -> Bool +gt = ordOp (\o -> case o of { GT -> True; _ -> False }) + + + +{- Operators: + + (x < y) => (lt ? ? x y) + (x <= y) => (le ? ? x y) + (x >= y) => (ge ? ? x y) + (x > y) => (gt ? ? x y) + +-} + + +-- +-- The Show class +-- + Show : Type -> Type Show A = sig { show : A -> String } show : (A : Type) -> Show A -> A -> String -show _ rec{show = show} x = show x - +show _ d = d.show + +show_Integer : Show Integer +show_Integer = rec { show = prim_show_Int } +-- +-- The Compos class +-- +Monoid : Type -> Type +Monoid = sig { mzero : A; mplus : A -> A -> A } Compos : (C : Type) -> (C -> Type) -> Type Compos C T = sig @@ -31,7 +150,7 @@ Compos C T = sig 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 +composOp _ _ d c f t = d.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 \ No newline at end of file +composFold _ _ d b m c f t = d.composFold b m c f t \ No newline at end of file