inductive map

Stream: new members

[Huỳnh Trần Khanh]

why is the "inductive map" construction the most common way to define a map? inductive map is like... the map is represented by a function from KeyType to ValueType, and the set key operation is implemented by function composition

[Huỳnh Trần Khanh]

why is it implemented by a function and not a list for example

[Huỳnh Trần Khanh]

of course a tree wouldn't be practical since that would require the key to support total ordering

[Mario Carneiro]

I'm not sure why you call that inductive, or most common

[Mario Carneiro]

it's certainly most general

[Huỳnh Trần Khanh]

https://github.com/blanchette/logical_verification_2020/blob/master/lean/lovelib.lean#L193

[Huỳnh Trần Khanh]

this is what I'm referring to

[Huỳnh Trần Khanh]

I have seen it several times in functional programming books

[Mario Carneiro]

it's convenient because it is easy to reason about

[Mario Carneiro]

it's not efficient at all

[Mario Carneiro]

it is basically a linear search built with thunks

[Mario Carneiro]

The important property you usually need about the lookup function is that it is equivalent to state.update

[Mario Carneiro]

so making it true by definition makes things easier

[Mario Carneiro]

it is possible to prove such a property for lookup functions implemented in a more efficient way, for example src#hash_map.mem_insert, but it is complicated and also comes with restrictions on the key type