[Haskell-cafe] looking for examples of non-full Functional
haberg at math.su.se
Fri Apr 25 10:37:08 EDT 2008
On 25 Apr 2008, at 15:38, Tom Schrijvers wrote:
>>> Prolog works under the assumption of a closed world. That's
>>> contrary to the open world view of regular type classes. So these
>>> aren't the intended semantics.
>> By which I gather you mean the interpretation of ":-" as logical
>> connective "=>" rather than provability "|-"?
> What I meant was that when Prolog says "there are no more
> solutions", it doesn't know of any more. In realtiy it means "there
> no more solutions under the closed world assumption". That means
> there could be more solutions if you haven't told Prolog
> everything. In this context, there may be more class instances (you
> simply haven't told the system yet).
I had no intention to deal with that problem. Just forget what Prolog
says, and when it says "there are no more solutions" think of it as
"no more solutions determined".
(If one interprets ":-" as provability "|-", there needs to be
additional axioms for the object theory, and if the theory is
consistent, it becomes possible to prove that there are no more
>> My point, though, was to interpret
>> class a b | a -> b
>> as a functional dependency b = b(a) rather than as
>> D a b, D a c ==> b=c
>> Thus trying to eliminate the use of "=".
> I don't follow you here.
?- instance(d, l(A), l(B)).
B = b(A)
?- instance(d, l(A), C).
C = l(b(A))
so pattern-wise C and l(B) are the same. But I do not bother
introduce an explicit operator "=". So at least in this case, if say
D [a] Int will be reject as Int is not of the feom l(_). If one has D
[Int] [Char] and tries to define D [Int] [Float], the leads to trying
to associate the implicit b(Int) with both Char and Float, which
would be rejected.
More information about the Haskell-Cafe