Status of Haskell Prime Language definition

[Iavor Diatchki]

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