Status of Haskell Prime Language definition
Iavor Diatchki
iavor.diatchki at gmail.com
Tue Oct 16 14:21:35 EDT 2007
Hello,
On 10/16/07, apfelmus <apfelmus at quantentunnel.de> wrote:
> Iavor Diatchki wrote:
> > apfelmus wrote:
> >> fundeps are too tricky to get powerful and sound at the same time.
> >
> > I am not aware of any soundness problems related to functional
> > dependencies---could you give an example?
>
> http://hackage.haskell.org/trac/haskell-prime/wiki/FunctionalDependencies#Lossofconfluence
>
> But I should have said "sound, complete and decidable" instead :)
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)
--
Iavor
More information about the Haskell-prime
mailing list