4 ms·
I haven't really explored this area of Haskell, but I think there are certain cases where this is possible. For example, I think there might be a way to have a
by thinkpad20 13y ago
I haven't really explored this area of Haskell, but I think there are certain cases where this is possible. For example, I think there might be a way to have a list of tuples of `forall a. [(a -> b, a)]`, where a's type can vary, but applying the first element of the tuple to the second will always produce a `b`. I'm not sure if this is actually the case but it seems (theoretically) possible, and certainly would be convenient. More experienced Haskellers feel free to chime in...
- tel 13y agoYeah, that's certainly possible. It's also largely frowned upon because it's usually over complex. For instance, in your example [exists a . (a -> b, a)] is literally completely equivalent to [b] as the types ensure there is no other thing that can be done with those pairs. The convenience factor is thus almost never the case. There are some nice theoretical properties and a great embedding of OO in Haskell via existential typing [0], but it should rarely be used. [0] http://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf http://www.cs.ox.ac.uk/jeremy.gibbons/publications/adt.pdf
- thinkpad20 13y agoOK, since I didn't give a very good example, let me try to show a better one. Let's imagine you're writing a testing library. You have a series of tests; each one of them takes in an input, a function to run on the input, and an expected output. data Test i o = Test String i (i -> o) o and then say your testing function is something like runTest :: Eq o => Test i o -> IO () runTest (Test name input f output) = case f input of o | o == output -> putStrLn $ name ++ " passed" | otherwise -> putStrLn $ name ++ " failed" Then let's say you had a bunch of tests. For example, you want to test that addition works: test1 = Test "addition" (1, 2) (\a b -> a + b) 3 And you want to test string concatenation: test2 = Test "concat" ("hello", "world") (\a b -> a ++ b) "helloworld" Then you could write your tests as doTests = runTest test1 >> runTest test2 Now if you have a lot of tests, it would be nice to put them in a list: doTests tests = forM_ tests runTest However, this would require that every test have the same inputs and outputs. You couldn't do doTests [test1, test2] Even though the resulting type is known (it will be an IO () regardless), and even though runTest will operate on each one, because test1 and test2 have different types, you can't put them all in a list. I think that `forall` and similar allow you to get around this restriction somehow, but I don't really know how that works.
- tel 13y agoI mean, I agree such examples exist. I don't think this is yet a truly good example, though. The real advantage to existential types like this are in creation of multiple variants---again I recommend reading Jeremy Gibbons' paper. But, for completeness, here's how you could write your type {-# LANGUAGE ExistentialQuantification #-} data Test = forall i o . Test i (i -> o) (o -> o -> Bool) o Although, note, this is exactly equivalent to `Bool`, although in two ways—if we knew the comparator function was commutative then there'd be just one way to convert to `Bool`. testBool :: Test -> Bool testBool (Test i fun cmp o) = cmp (fun i) o testBool' :: Test -> Bool testBool' (Test i fun cmp o) = cmp o (fun i) But in either case there are no other ways to "observe" the existentially quantified types since we've forgotten absolutely everything besides `Bool`. More likely we would want to also, say, show the input. data Test = forall i o . (Eq o, Show i) => Test i (i -> o) o and this type is now equal to `(String, Bool)`. testOff :: Test -> (String, Bool) testOff (Test i fun o) = (show i, fun i == o) So, in general, if you're using existential types you really want to either be using multiple variants or when you have such a combination of observables that it's not worth expressing them all directly.