Status of Haskell Prime Language definition
apfelmus
apfelmus at quantentunnel.de
Thu Oct 18 05:54:35 EDT 2007
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
More information about the Haskell-prime
mailing list