Thu, 27 Jul 2000 23:59:47 +0100, Claus Reinke <[EMAIL PROTECTED]> pisze:
> Whenever a type is qualified by a class context, this establishes
> a proof obligation for the class mechanism, and while this mechanism
> tries to complete the proof, it also collects and composes the
> functional program( fragment)s attached to the rules and facts
> used in the proof.
But because the proof itself is essential, there is an unusual
requirement for proofs that there must exist exactly one proof. The
theorem must sometimes be explicitly strengthened to restrict possible
proofs to a single choice.
It is necessary for sane semantics, but it can be annoying. The
language must provide ways to constrain statements: explicit type
signatures, functional dependencies, possibly improvement, and finally
the standard defaulting rule that introduces an exception in the
requirement of a unique proof.
> [In fact, termination is no longer seen as a must, as long as
> programmers don't get bitten. Anyone willing to relax the
> determinism restriction, letting the programmer choose at
> compile-time from a set of alternatives enumerated by the
> compiler?-)]
GHC already does that. -fallow-undecidable-instances relaxes accepted
forms of instance declarations and prevents infinite looping by
bounding the depth of recursion.
> Back to our callN-problem:
> If I'm not mistaken, you've actually encountered two limitations
> of the current class mechanism at once:
>
> 1. Invoking the class mechanism to resolve a type constraint
> will never instantiate variables in the original qualified type.
Fundeps do this.
Unfortunately they can be only applied uniformly to all instances of
a class. I have for example instances:
instance ForeignArg (Ptr a) (Ptr a)
instance Storable a => ForeignArg (Ptr a) a
instance Storable a => ForeignArg (Ptr a) [a]
Luckily they don't overlap, because second type of each pair contains a.
They did overlap when the last case was ForeignArg (Ptr [a]) [a].
I would like to say that in the instance ForeignArg (Ptr a) (Ptr a)
the first Ptr a together with the second Ptr determine the second a.
The second a is not "input" (the instance matches when it has a here)
but "output" (when the rest matches then here is a). Other possible
constraints here are not essential, but this one would avoid some
need of explicit type signatures, including the big one which is
Ptr (StablePtr a) -> CSize -> CSize -> FunPtr (Ptr (StablePtr a) ->
Ptr (StablePtr a) -> IO CInt) -> IO ().
Similarly, I have another instance:
instance ForeignRes (Ignore a) ()
and would like to say that Ignore a determines that the second type is ().
> 2. As you noticed, there is no way to get the equivalent of
> Prolog's closed-world assumption - we can't tell the class
> mechanism that the instances currently in sight are all the
> instances that will ever be available.
Fundeps workaround this in some cases. They disallow adding particular
forms of further instances, making the world smaller, thus allowing
the compiler to disambiguate a bit. I wonder if fundeps can be extended
to express the above statement.
Instances themselves already disallow some further instances: namely
for types that unify. Fundeps refine that but they are still too
imprecise.
> So your example can be reduced further:
>
> ----------------------------------
> module Class where
>
> class C t
> instance C Double
>
> f:: C a => a
> f = 1
>
> g:: C Int => Int
> g = 2
> ----------------------------------
I believe that
class C t | -> t
should solve this.
GHC does not accept f nor g, but Hugs does accept f with its context
extended to (C a, Num a). The inferred type for f, as shown by :t f,
is Double. Hugs does compile g, but any attempt to use it yields:
ERROR: Constraints are not consistent with functional dependency
*** Constraint : C Int
*** And constraint : C Double
*** For class : C a
*** Break dependency : -> a
An alternative with fundeps refined in instances should work as well.
--
__("< Marcin Kowalczyk * [EMAIL PROTECTED] http://qrczak.ids.net.pl/
\__/ GCS/M d- s+:-- a23 C+++$ UL++>++++$ P+++ L++>++++$ E-
^^ W++ N+++ o? K? w(---) O? M- V? PS-- PE++ Y? PGP+ t
QRCZAK 5? X- R tv-- b+>++ DI D- G+ e>++++ h! r--%>++ y-
