mirror of
https://github.com/anoma/juvix.git
synced 2024-12-15 01:52:11 +03:00
08f123fa3d
* Closes #1646 Implements a basic trait framework. A simple instance search mechanism is included which fails if there is more than one matching instance at any step. Example usage: ``` import Stdlib.Prelude open hiding {Show; mkShow; show}; trait type Show A := mkShow { show : A → String }; instance showStringI : Show String := mkShow (show := id); instance showBoolI : Show Bool := mkShow (show := λ{x := if x "true" "false"}); instance showNatI : Show Nat := mkShow (show := natToString); showList {A} : {{Show A}} → List A → String | nil := "nil" | (h :: t) := Show.show h ++str " :: " ++str showList t; instance showListI {A} {{Show A}} : Show (List A) := mkShow (show := showList); showMaybe {A} {{Show A}} : Maybe A → String | (just x) := "just (" ++str Show.show x ++str ")" | nothing := "nothing"; instance showMaybeI {A} {{Show A}} : Show (Maybe A) := mkShow (show := showMaybe); main : IO := printStringLn (Show.show true) >> printStringLn (Show.show false) >> printStringLn (Show.show 3) >> printStringLn (Show.show [true; false]) >> printStringLn (Show.show [1; 2; 3]) >> printStringLn (Show.show [1; 2]) >> printStringLn (Show.show [true; false]) >> printStringLn (Show.show [just true; nothing; just false]) >> printStringLn (Show.show [just [1]; nothing; just [2; 3]]) >> printStringLn (Show.show "abba") >> printStringLn (Show.show ["a"; "b"; "c"; "d"]); ``` It is possible to manually provide an instance and to match on implicit instances: ``` f {A} : {{Show A}} -> A -> String | {{mkShow s}} x -> s x; f' {A} : {{Show A}} → A → String | {{M}} x := Show.show {{M}} x; ``` The trait parameters in instance types are checked to be structurally decreasing to avoid looping in the instance search. So the following is rejected: ``` type Box A := box A; trait type T A := mkT { pp : A → A }; instance boxT {A} : {{T (Box A)}} → T (Box A) := mkT (λ{x := x}); ``` We check whether each parameter is a strict subterm of some trait parameter in the target. This ordering is included in the finite multiset extension of the subterm ordering, hence terminating. |
||
|---|---|---|
| .. | ||
| Base.hs | ||
| Negative.hs | ||
| Positive.hs | ||