AshleyYakeley / Truth

Changes and Pinafore projects. Pull requests not accepted.
https://pinafore.info/
GNU General Public License v2.0
32 stars 0 forks source link

Hash-map type #214

Closed AshleyYakeley closed 11 months ago

AshleyYakeley commented 11 months ago
type storable Map +a;
lookup: Entity -> Map a -> Maybe a;
empty: Map None;
insert: Entity -> a -> Map a -> Map a;
delete: Entity -> Map a -> Map a;
singleton: Entity -> a -> Map a;
(<>): Map a -> Map a -> Map a;
keys: Map Any -> List Entity;
values: Map a -> List a;
toList: Map a -> List (Entity *: a);
fromList: List (Entity *: a) -> Map a;
AshleyYakeley commented 11 months ago
type storable Map +k +v;
lookup: k & Entity -> Map k v -> Maybe v;
empty: Map None None;
insert: k & Entity -> v -> Map k v -> Map k v;
delete: k & Entity -> Map k v -> Map k v;
singleton: k -> v -> Map k v;
(<>): Map k v -> Map k v -> Map k v;
keys: Map k v -> List k;
values: Map k v -> List v;
toList: Map k v -> List (k *: v);
fromList: List (k & Entity *: v) -> Map k v;
(.): Map vk v -> Map k vk -> Map k v;

Can't have covariant k parameter (and therefore storability), because this mapping cannot be done without Ord restriction.

AshleyYakeley commented 11 months ago

also an arbitrary (numeric) ordering on Entity:

entityOrder: Entity -> Entity -> Ordering
AshleyYakeley commented 11 months ago
data LangMap {kp,kq} v where
    MkLangMap :: Ord k => (kp -> k) -> (k -> kq) -> Map k v -> LangMap {kp,kq} v

or

data LangMap {kp,kq} v where
    MkLangMap :: (kp -> Entity) -> Map Entity (kq,v) -> LangMap {kp,kq} v
type Map {-kp,+kq} +v;
lookup: k -> Map -k v -> Maybe v;
empty: Map {} None;
insert: kp -> v -> Map {-kp,+kq} v -> Map {-kp,+kq} v;
delete: kp -> Map {-kp,+kq} v -> Map {-kp,+kq} v;
singleton: k & Entity -> v -> Map k v;
(<>): Map k v -> Map k v -> Map k v;
keys: Map +k Any -> List k;
values: Map Any v -> List v;
toList: Map +k v -> List (k *: v);
fromList: List (k & Entity *: v) -> Map k v;
(.): Map vk v -> Map k vk -> Map k v;
AshleyYakeley commented 11 months ago

Done.