Created map type is always first defined map type

[saulshanabrook]

I have noticed a slight oddity in the current type system. The order in which you defined map sorts influences the type of maps you create.

Example

For example, this works:

(sort MyMap (Map i64 String))
(sort MyMap1 (Map i64 i64))

(define my_map1 (insert (empty) 1 "one"))

whereas this fails:

(sort MyMap1 (Map i64 i64))
(sort MyMap (Map i64 String))

(define my_map1 (insert (empty) 1 "one"))

This means you cannot create two different types of maps in one level.

Why does it happen

When you register a map sort, like (sort MyMap (Map i64 String)), this will register the primitives, including create. If you do this twice, then two primitives will be registered under the name create. However, when you call create, the first one registered will be chosen.

Workaround

You can get around this by pushing a level, creating a map, then going up a level:

(push)
(sort MyMap1 (Map i64 i64))
(define my_map1 (insert (empty) 1 1))
(pop)

(sort MyMap (Map i64 String))

(define my_map2 (insert (empty) 1 "one"))

Solution

I am not sure if there an elegant way to address this oddity at the moment. I am not sure if it would be classified as a bug.

My understanding of the underlying issue is that type system of egg-smol is mainly the simply typed lambda calculus. Users can create custom type (sorts) and define function which map between different types. Users cannot create functions that are generic or create types that depend on other types.

Builtin maps are supported as the only parametric types, but they are added in such a way as to make them appear as simple types.

This leads to this issue, since there is no way to pass a type into a function. To solve it, I believe we would need to be able to pass a type into the create function to parameterize it with something like (create (Map i64 i64)) or (create i64 i64).

This would mean changing the type system of egg-smol from a simply typed lambda calculus to the System Fω, since it requires having types that depend on types (Map) and terms that depend on types (create). This would also allow users to define other custom types, such as lists or simply typed functions (like a lambda from int to str).

I am not suggesting this one oddity would be enough motivation for such a large change, since it is possible to work around it currently. But I wanted to open this issue to write out my thoughts here, since I had been thinking about the possibility of adding user-defined parametrics for a while :)

Thanks for all the work on this library! It's very exciting.

[mwillsey]

Thanks for the issue! I think we are planning to rework the type system / at least the type checker soon.

[hackedy]

I think I just got bitten by this one? Here is a reduced counterexample

(sort IntMap (Map i64 i64))
(sort SetOfMaps (Map IntMap i64))

(datatype Sets
  (Set SetOfMaps))

(function emp (Sets Sets) i64)
(rewrite (emp (Set (empty))) 1)

The error is

Local already bound v2___ with type IntMap. Got: SetOfMaps

[yihozhang]

Just a note that this is not fixed by #219 because #219 only adds constraint-based inference for queries not actions.

[yihozhang]

Fixed by #320