Lack of unification prevents true separation of data and type "schema"

[deepfire]

Lack of unification prevents true separation of data and type "schema"

[deepfire]

This is somewhat related to #73

[Gabriella439]

Yeah, this will likely be the case for the foreseeable future

The main reason why Dhall is designed this way is because Dhall is "completely functional" meaning that there is no logic programming component (whether at the type-level or otherwise) and therefore no unification. All automation in Dhall is based around functions, including type-level automation. This is why type abstraction and type application are explicit. If something is repetitive you use a function to reduce the repetition.

Dhall is also based on a "pure type system" which means that there is no syntactic distinction between term-level programming and type-level programming. This is why you use the notation to abstract and apply types and terms. This is also why you use the same let notation to define type synonyms and you can also (more recently on master) store types in records/unions. Because there isn't a strict separation between the term and type level there will never really be a separation of data and schema.

That does mean that it is less ergonomic in the small but it also means that it is far more straightforward to debug and errors are better localized because type inference is only done in the forward direction. It also makes the type-checking algorithm easier to explain and reason about because there is no subtyping relationship between polymorphic and monomorphic terms and the conversions between them are explicit instead of implicit.

[Gabriella439]

I will go ahead and close this, but feel free to reopen if there are additional questions