] On Behalf Of Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Cc: glasgow-haskell-users@haskell.org; Haskell Cafe
| Subject: Re: Advice on type families and non-injectivity?
|
| Hi Conal,
|
| I agree that your initial example is a little puzzling, and I'm glad
| that the new
[mailto:glasgow-haskell-
| users-boun...@haskell.org] On Behalf Of Richard Eisenberg
| Sent: 14 January 2013 03:47
| To: Conal Elliott
| Cc: glasgow-haskell-users@haskell.org; Haskell Cafe
| Subject: Re: Advice on type families and non-injectivity?
|
| Hi Conal,
|
| I agree that your initial example
Thanks, Jake! This suggestion helped a lot. -- Conal
On Sun, Jan 13, 2013 at 1:59 PM, Jake McArthur jake.mcart...@gmail.comwrote:
I have a trick that loses a little convenience, but may still be more
convenient than data families.
{-# LANGUAGE TypeFamilies #-}
import Data.Tagged
type
On Mon, Jan 14, 2013 at 3:39 AM, Simon Peyton-Jones
simo...@microsoft.com wrote:
There is a real difficulty here with type-checking 'bar'. (And that
difficulty is why 'foo' is also rejected.)
This seems, to me, like a somewhat round-about way to express the
problem. Iavor's explanation (which
: Richard Eisenberg; glasgow-haskell-users@haskell.org; Haskell Cafe
Subject: Re: Advice on type families and non-injectivity?
There is a real difficulty here with type-checking 'bar'. (And that difficulty
is why 'foo' is also rejected.)
Oh! Is the definition of 'foo' rejected in recent versions
I sometimes run into trouble with lack of injectivity for type families.
I'm trying to understand what's at the heart of these difficulties and
whether I can avoid them. Also, whether some of the obstacles could be
overcome with simple improvements to GHC.
Here's a simple example:
{-# LANGUAGE
Hi,
How would you infer a from F a? Given bar :: Bool, I can't see how
one could go from Bool to F a = Bool and determine a uniquely.
My question is not completely retorical, if there is an answer I would
like to know it :-)
Gruss,
Christian
* Conal Elliott co...@conal.net [13.01.2013 20:13]:
Hello Conal,
The issue with your example is that it is ambiguous, so GHC can't figure
out how to instantiate the use of `foo`. It might be easier to see why
this is if you write it in this form:
foo :: (F a ~ b) = b
foo = ...
Now, we can see that only `b` appears on the RHS of the `=`, so
Hi Iavor,
Thanks for the remarks.
so there is really no way for GHC to figure out what is the intended value
for `a`.
Indeed. Though I wonder: does the type-checker really need to find a
binding for `a` in this case, i.e., given the equation `(forall a. F a) ==
(forall a'. F a')`?
-- Conal
Hi Christian,
Given bar :: Bool, I can't see how one could go from Bool to F a =
Bool and determine a uniquely.
The same question applies to foo :: Bool, right? Yet no error message
there.
Regards, - Conal
On Sun, Jan 13, 2013 at 11:36 AM, Christian Höner zu Siederdissen
Hello,
On Sun, Jan 13, 2013 at 12:05 PM, Conal Elliott co...@conal.net wrote:
so there is really no way for GHC to figure out what is the intended value
for `a`.
Indeed. Though I wonder: does the type-checker really need to find a
binding for `a` in this case, i.e., given the equation
Hi Conal,
if you take your example program and write foo :: Bool, ghci accepts it?
For me it complains, and I would think rightly so, that couldn't match
expected type Fa with actual type Bool. It actually only works with the
following quite useless type instance F a = Bool.
By the way, using
Hi Conal,
I agree that your initial example is a little puzzling, and I'm glad that the
new ambiguity checker prevents both definitions, not just one.
However, your initial question seems broader than just this example. I have run
into this problem (wanting injective type functions) several
13 matches
Mail list logo
