class C a b | a->b where
op :: a -> b
instance C Int Bool where
op n = n>0
data T a where
T1 :: T a
T2 :: T Int
-- Does this typecheck?
f :: C a b => T a -> Bool
f T1 = True
f T2 = op 3
The function f "should" typecheck because inside the T2 branch we know
that (a~Int), and hence by the fundep (b~Bool).
Perhaps I'm confused, but there seems to be no link between
the call 'op 3' and 'a' in this example. While the 'desugaring'
introduces just such a connection.
g :: C a b => TT a -> Bool
g TT1 = True
g (TT2 eq) = op (if False then cast eq undefined else 3)
If we add that connection to the original example, it typechecks
as well:
f :: forall a b. C a b => T a -> Bool
f T1 = True
f T2 = op (3::a)
We could also write:
f :: forall a b. C a b => T a -> Bool
f T1 = True
f T2 = (op :: a -> Bool) 3
Though there is a long-standing issue that we cannot write
f :: forall a b. C a b => T a -> Bool
f T1 = True
f T2 = (op :: a -> b) 3
as that results in the counter-intuitive
Couldn't match expected type `Bool' against inferred type `b'
`b' is a rigid type variable bound by
the type signature for `f'
at C:\Users\claus\Desktop\tmp\fd-local.hs:17:14
In the expression: (op :: a -> b) 3
In the definition of `f': f T2 = (op :: a -> b) 3
Which seems to be a variant of Oleg's example? I thought there
was a ticket for this already, but I can't find it at the moment. It
would be useful to have standard keywords (FD, TF, ..) to make
ticket querying for common topics easier, and to record the
status of FD vs TF in trac.
There used to be a difference the other way round as well
(more improvement with FDs than with TFs), which I found
while searching trac for the other issue:
http://hackage.haskell.org/trac/ghc/ticket/2239
From testing that example again with 6.12.3, it seems that
bug has since been fixed but the ticket not closed?
But we have no formal type system for fundeps that describes this,
and GHC's implementation certainly rejects it.
I've not yet finished Martin's paper, and your recent major work
is also still on my reading heap, but just to get an idea of the
issues involved: from CHR-based fundep semantics, the step
to local reasoning would seem to encounter hurdles mainly in
the interaction of local and non-local reasoning, right?
If we only wanted to add local reasoning, the standard solution
would be to make copies, so that the local steps don't affect the
global constraint store (somewhat more practical, we could add
tags to distinguish local and global stores; for sequential
implementations, Prolog-style variable trails could probably be
extended to account for constraints as well).
But we want local reasoning to make use of non-local constraints
and variable bindings, and we probably want to filter some, but
not all, local reasoning results back into the global store.
Are these the issues, or are there others?
Claus
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
