@scull7: Yeah, that is correct. { Thing = {} }
and { Thing : {} }
are two separate things. The former one is a record literal whose values are types and the latter one is a record type whose field is also a record type.
The latter idiom of { Thing : {} }
is much more common, but there are two use-cases for the former idiom of { Thing = {} }
:
-
First, Dhall packages are records, so you can think of { Thing = {} }
as like a Dhall package that exports a type named Thing
-
Second, you can use a record whose fields are types to name type arguments, like this:
let Map =
λ(args : { key : Type, value : Type }) →
List { mapKey : args.key, mapValue : args.value }
in toMap { foo = 1 } : Map { key = Text, value = Natural }