Iavor Diatchki wrote:
http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies#Lossofconfluence
There is nothing about the system being unsound there. Furthermore, I
am unclear about the problem described by the link... The two sets of
predicates are logically equivalent (have the same set of ground
instances), here is a full derivation:
(B a b, C [a] c d)
using the instance
(B a b, C [a] c d, C [a] b Bool)
using the FD rule
(B a b, C [a] c d, C [a] b Bool, b = c)
using b = c
(B a b, C [a] c d, C [a] b Bool, b = c, C [a] b d)
omitting unnecessary predicates and rearranging:
(b = c, B a b, C [a] b d)
The derivation in the other direction is much simpler:
(b = c, B a b, C [a] b d)
using b = c
(b = c, B a b, C [a] b d, C [a] c d)
omitting unnecessary predicates
(B a b, C [a] c d)
You're right, I think I'm mixing up soundness with completeness and
termination. My thought was that not explicitly mentioning the b=c
constraint could lead to the type inference silently dropping this fact
and letting an inconsistent set of instance declarations "go through"
without noticing. But that would only be important in a setting where
inconsistent instances are not reported early via the consistency
condition but late when actually constructing terms. The consistency
condition should be enough for soundness (no inconsistent axioms
accepted), but I didn't dwell enough into FD to know such things for sure.
Regards,
apfelmus
_______________________________________________
Haskell-prime mailing list
Haskell-prime@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-prime
