In article
[EMAIL PROTECTED]
ft.com,
Simon Peyton-Jones [EMAIL PROTECTED] wrote:
Here's a less complicated variant of the same problem:
class C a b | a - b where {}
instance C Int Int where {}
f :: (C Int b) = Int - b
f x = x
Is the defn of f legal? Both
Ashley Yakeley wrote:
If this were allowed, it would effectively allow type-lambda
class C a b | a - b
instance C Int Bool
instance C Bool Char
newtype T a = MkT (forall b.(C a b) = b)
helperIn :: (forall b.(C a b) = b) - T a
helperIn b = MkT b; -- currently won't work
helperOut :: T a
| I believe something along the lines of the following would work:
|
| class C a b | a - b where { foo :: b - String }
| instance C Int Int where { foo x = show (x+1) }
| x :: forall b. C Int b = b
| x = 5
|
| (Supposing that the above definition were valid; i.e., we didn't get
the
| type
| The reason, which is thoroughly explained in Simon Peyton-Jones'
| message, is that the given type signature is wrong: it should read
| f1 :: (exists b. (C Int b) = Int - b)
|
| Right. Simon pointed out that this is a pretty useless function, but
not
| entirely so, since the result of
| entirely so, since the result of it is not of type 'forall b. b', but
| rather of 'forall b. C Int b = b'. Thus, if the C class has a
function
| which takes a 'b' as an argument, then this value does have use.
I disagree. Can you give an example of its use?
I believe something
| The reason, which is thoroughly explained in Simon Peyton-Jones'
| message, is that the given type signature is wrong: it should read
| f1 :: (exists b. (C Int b) = Int - b)
Can you give an example of its use?
Yes, I can.
class (Show a, Show b) = C a b | a - b where
doit:: a -
| since this claims that it will take a Bool and produce a value of type
b
| for all types b. However, would it be all right to say (in
| pseudo-Haskell):
|
| f :: exists b . Bool - b
| f x = x
But this is a singularly useless function, because it produces a result
of utterly unknown type, so
The reason, which is thoroughly explained in Simon Peyton-Jones'
message, is that the given type signature is wrong: it should read
f1 :: (exists b. (C Int b) = Int - b)
Right. Simon pointed out that this is a pretty useless function, but not
entirely so, since the result of it is not
Hello!
It seems we can truly implement Monad2 without pushing the
envelope too far. The solution and a few tests are given below. In
contrast to the previous approach, here we lift the type variables
rather than bury them. The principle is to bring the type logic
programming at the level
Interesting example
| class Monad2 m a ma | m a - ma, ma - m a where
| return2 :: a - ma
| bind2 :: Monad2 m b mb = ma - (a - mb) - mb
| _unused :: m a - ()
| _unused = \_ - ()
| instance Monad2 [] a [a] where
| bind2 = error urk
The functional dependencies say
m a -
Hi Simon, all,
Here's a less complicated variant of the same problem:
class C a b | a - b where {}
instance C Int Int where {}
f :: (C Int b) = Int - b
f x = x
This is interesting, but I'm not entirely sure what the problem is (from a
theoretical, not
Hello!
Simon Peyton-Jones wrote:
class C a b | a - b where {}
instance C Int Int where {}
f1 :: (forall b. (C Int b) = Int - b)
f1 x = undefined
Indeed, this gives an error message
Cannot unify the type-signature variable `b' with the type `Int'
Expected type: Int
Suppose we are in case 1. Then the programmer has written a too-general
type signature on f. The programmer *must* know that b=Int in this case
otherwise his function definition makes no sense. However, I don't really
see a reason why this should be an error rather than just a warning. If
The reason, which is thoroughly explained in Simon Peyton-Jones'
message, is that the given type signature is wrong: it should read
f1 :: (exists b. (C Int b) = Int - b)
Sigh, read this after posting :)
___
Haskell mailing list
[EMAIL
14 matches
Mail list logo