Continuing a bit on the subject posted on this thread, I have run into two cases where a function produces identical outcomes for all input but has different hashes. Both came up when I was refactoring dhall code, which gave me the spooks as I was pretty sure my logic hadn’t changed, so I had to run several examples a la quickcheck just to convince myself it hadn’t.
Case 1
let Natural/equal : Natural -> Natural -> Bool =
https://prelude.dhall-lang.org/Natural/equal
sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
let neq: Natural -> Natural -> Bool = \(n0: Natural) -> \(n1: Natural) -> Natural/equal n0 n1
in neq
yields a hash sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
, whereas
let Natural/equal : Natural -> Natural -> Bool =
https://prelude.dhall-lang.org/Natural/equal
sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
let neq: Natural -> Natural -> Bool = \(n0: Natural) -> \(n1: Natural) -> Natural/equal n1 n0
in neq
yields a hash sha256:9e0e952e097a2a974ca4ed3e65bcf395cda2bb54382c8ecc3963bca50bfff124
.
Case 2
let Natural/equal : Natural -> Natural -> Bool =
https://prelude.dhall-lang.org/Natural/equal
sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
let User: Type = { id : Natural, name : Text }
let userEq: User -> User -> Bool = \(u0: User) -> \(u1: User) -> Natural/equal u0.id u1.id
in userEq
Yields a hash of sha256:9dd6204f24c38fec828b454492d37086018b2781b2189f5e270d824055a2fe20
whereas
let Natural/equal : Natural -> Natural -> Bool =
https://prelude.dhall-lang.org/Natural/equal
sha256:7f108edfa35ddc7cebafb24dc073478e93a802e13b5bc3fd22f4768c9b066e60
let User: Type = { id : Natural, name : Text, email : Text }
let userEq: User -> User -> Bool = \(u0: User) -> \(u1: User) -> Natural/equal u0.id u1.id
in userEq
yields a hash of sha256:9c5e711166f46d9c69f6fc1d2cf4dd2dc7c14495f9ae60259fa27f468c1cc1f0
.
Comments
The two cases are different, and perhaps this is intended behavior, but it caught me by surprise so maybe there is a way to document it? In general, like my first post, it is getting at issues of extensionality in Dhall. Basically, I’m trying to avoid experimenting with heavier solutions like z3
or coq
for verifying that certain configurations haven’t changed, and if I can bend dhall to do this that’d be great as my configurations are in dhall anyway and it’d prevent me from using another tool/language.
Thanks for your help!