Builtin Map type

[mmhat]

When working with Dhall every now and then I with for something that is a record, but with a fixed type for all the fields. Records have the advantage that we can address fields by name (record_value.field_name) but we cannot talk about the types of the fields. Lists have the advantage that we can do this - for instance, we can map over the elements - but we cannot address an element in a type-safe way. The idea is to have something combining both, i.e. a homogenous record. But it might be better to call it a Map (or an Object or a Dictionary). Since we have subtyping in this language this type would probably a subtype of Record and can be easily converted to a List.

A first idea for the syntax: {! field1 : value1, field2 : value1, ... }, i.e. the only difference is the exclamation mark after the opening brace (no whitespace allowed inbetween - it parses as one token). This has the disadvantage that it might be easily confused with a record when one is skimming through some source code but on the other hand it one can quickly change a Record type to a Map type.

[Gabriella439]

If we do the subtyping right then we might not even need a new syntax. In other words, if a homogeneous record is a subtype of a Map then users would be able to use record syntax anywhere a Map was expected

I'll provide two concrete examples to illustrate what I mean:

• Suppose that we provided a builtin of type Map/map : forall (a : Type) . forall (b : Type) . Map a -> Map b

  Then the user would be able to write:

  Map/map Natural/even { foo: 0 }

  … and the result would be:

  { foo: true } : Map Bool

• Users could always downgrade a record to a Map by just adding a type annotation (if it cannot be inferred from the context)

  { foo: 0 } : Map Natural

[mmhat]

Hm, I guess we are talking about different things here. Maybe Map was the wrong name for what I meant. Consider the following program:

let isEven = Map/map Natural/even

let getFoo = \x -> x.foo

let f = \x -> getFoo (isEven x)

in
f

If I am not mistaken then Grace would infer isEven : Map Natural -> Map Bool and getFoo : forall (a : Type) . forall (b : Fields) . { foo: a, b } -> a. But f shouldn't type check because it would involve an unsafe upgrade of the type from a Map to a record type. By "unsafe" I mean that Grace cannot know from the type Map Bool that this map has the field foo.
That was at least my assumption when I proposed the syntax in the opening comment. It is a similar situation we have with the Map type found in the Dhall prelude: The lookup of a key must return an Optional value since we do not know from the type if that key is present in the map or not.

What I had in mind when I opened this issue was a type that has both properties: A type-safe lookup (no Optional) and the ability to map over the values. As for the example grace would infer f : forall (b : Fields) . {! foo: Natural, b } -> Bool or f : forall (b : Fields) . { foo: Natural, b } -> Bool depending on the syntax we choose.

Hope this makes it a bit clearer what my idea was. Does it make sense?

[Gabriella439]

What would the type of Map/map be?

[mmhat]

What would the type of Map/map be?

That is indeed a good question. It is not yet clear to me; Maybe

Map/map : forall (a : Type) . forall (b : Type) . forall (fa : MapFields a) . forall (fb : MapFields b) . (a -> b) -> { fa } -> { fb }

or

Map/map : forall (a : Type) . forall (b : Type) . forall (f : MapFields) . (a -> b) -> { f a } -> { f b }

or

Map/map : forall (a : Type) . forall (b : Type) . forall (f : Type -> Fields) . (a -> b) -> { f a } -> { f b }

?