Hi! I’ve been having a chat with Fabrizio about dhall and he recommended I post some of the questions here to the broader community. I’m looking forward to getting to know y’all!
I am wondering what the limits of dhall’s normalized form are for functions and if there is a roadmap for future development. For example, normalized form on arithmetic is not yet supported in some cases:
PS C:\Users\MikeSolomon\devel\random-scripts\dhall> "\(n : Natural) -> [ n, n + 3 ]" | .\dhall.exe hash
sha256:8b215570802fe99fe3ba60a9bc9a81015a5c831e662d1fccf6521ad2b9831a3f
PS C:\Users\MikeSolomon\devel\random-scripts\dhall> "\(n : Natural) -> [ n, n + 1 + 2 ]" | .\dhall.exe hash
sha256:9250fbfabd94c822ad2e530b857b04c097ee0a5c6f7a64a8c29d7103f867619e
While it is supported in other cases:
PS C:\Users\MikeSolomon\devel\random-scripts\dhall> "\(n : Natural) -> 1 + 1" | .\dhall.exe hash
sha256:ea410b604b0eb8f0c9f9c77c30c2c40222829f6ccdc8ca600a7a2fb51bedebbd
PS C:\Users\MikeSolomon\devel\random-scripts\dhall> "\(n : Natural) -> 2" | .\dhall.exe hash
sha256:ea410b604b0eb8f0c9f9c77c30c2c40222829f6ccdc8ca600a7a2fb51bedebbd
The background is that I’m doing an experiment using dhall to compare pure functions, and I would like any functions that have the same behavior to have the same hash (extensionality). This is of course quite hard to do and impossible for a Turing complete language, but as dhall is not Turing complete I thought that this sort of thing may be worth discussing and knowing more about.
Thanks in advance for any thoughts/info about this!