"S. Alexander Jacobson" wrote:
>
> Do existential types makes algebraic types obsolete?
> I mean there seems to be a large semantic overlap between the two
> concepts.
<snip for brevity>
> Are there contexts where you need algebraic types because existential
> types won't do the job? Wouldn't everybody be happier if you could just
> pattern match on type names (someone else requested this in a recent
> thread)?
I'm not exactly sure what you are asking in regard to existential types
vs. algebraic types, but I wanted to respond in response to your last
question about pattern matching on types. I believe that you are
referring to a statement I had made in some other thread. What I
envisioned with such a concept would not necessarily reduce the need for
algebraic types but rather type classes. (Maybe it would reduce the need
for both. I haven't thought about it much.) To take your example of
TypeName:
> typeName :: a -> String
> typeName (x :: True) = "True"
> typeName (x :: False) = "False"
> typeName (x :: Int) = "Int"
> typeName _ = "Unknown"
The problem with this concept, as I have it written out, is that it is
dependent upon the ordering of the patterns. For example, if in one
module we define the following:
> write :: a -> b -> IO ()
> write (ref :: IORef a) (x :: a) = writeIORef ref x
> write (_ :: TTY) (x :: String) = print x
> write _ (e :: Error) = exitWith (errorVal e)
And in a different module, we define:
> write (_ :: MVar String) x = putMVar mvar (show x)
What would happen if `write' was called with an MVar variable and an
Error variable? Would the `exitWith' function get called, or would the
`putMVar' function get called?
I'm sure that several people have already thought of this before and
have written papers about it and even given it a name. But I'm a hacker
working in the trenches; I'm not solely interested in theory, I want
something that makes my life easier.
On a related note, can anyone point out a good document that lists the
difference between universal quantification, existential quantification,
and "normal" quantification. I assume that normal quantification /is/
universal quantification, but why would someone desire to be explicit?
Under what circumstances does it make sense to use existential
quantification? It would be helpful if such a document used valid
examples (i.e., no functions or types named "foo") so that I can see
what Read World(tm) problem is being solved.
- Michael Hobbs
