CODEWITHSUNDEEP
haskellgadtexistential-type
Alexey Romanov
Alexey Romanov

Reputation: 170919

Is this use of GADTs fully equivalent to existential types?

Existentially quantified data constructors like

data Foo = forall a. MkFoo a (a -> Bool)
         | Nil

can be easily translated to GADTs:

data Foo where 
    MkFoo :: a -> (a -> Bool) -> Foo
    Nil :: Foo

Are there any differences between them: code which compiles with one but not another, or gives different results?

Upvotes: 4

Views: 451

Answers (3)

chi
chi

Reputation: 116174

They are nearly equivalent, albeit not completely so, depending on which extensions you turn on.

First of all, note that you don't need to enable the GADTs extension to use the data .. where syntax for existential types. It suffices to enable the following lesser extensions.

{-# LANGUAGE GADTSyntax #-}
{-# LANGUAGE ExistentialQuantification #-}

With these extensions, you can compile

data U where
    U :: a -> (a -> String) -> U

foo :: U -> String
foo (U x f) = f x

g x = let h y = const y x
      in  (h True, h 'a')

The above code also compiles if we replace the extensions and the type definition with

{-# LANGUAGE ExistentialQuantification #-}
data U = forall a . U a (a -> String)

The above code, however, does not compile with the GADTs extension turned on! This is because GADTs also turns on the MonoLocalBinds extension, which prevents the above definition of g to compile. This is because the latter extension prevents h to receive a polymorphic type.

Upvotes: 9

Carl
Carl

Reputation: 27023

The latter isn't actually a GADT - it's an existentially quantified data type declared with GADT syntax. As such, it is identical to the former.

The reason it's not a GADT is that there is no type variable that gets refined based on the choice of constructor. That's the key new functionality added by GADTs. If you have a GADT like this:

data Foo a where
    StringFoo :: String -> Foo String
    IntFoo :: Int -> Foo Int

Then pattern-matching on each constructor reveals additional information that can be used inside the matching clause. For instance:

deconstructFoo :: Foo a -> a
deconstructFoo (StringFoo s) = "Hello! " ++ s ++ " is a String!"
deconstructFoo (IntFoo i)    = i * 3 + 1

Notice that something very interesting is happening there, from the point of view of the type system. deconstructFoo promises it will work for any choice of a, as long as it's passed a value of type Foo a. But then the first equation returns a String, and the second equation returns an Int.

This is what you cannot do with a regular data type, and the new thing GADTs provide. In the first equation, the pattern match adds the constraint (a ~ String) to its context. In the second equation, the pattern match adds (a ~ Int).

If you haven't created a type where pattern-matching can cause type refinement, you don't have a GADT. You just have a type declared with GADT syntax. Which is fine - in a lot of ways, it's a better syntax than the basic data type syntax. It's just more verbose for the easiest cases.

Upvotes: 4

Dominique Devriese
Dominique Devriese

Reputation: 3093

From the documentation:

Notice that GADT-style syntax generalises existential types (Existentially quantified data constructors). For example, these two declarations are equivalent:

data Foo = forall a. MkFoo a (a -> Bool)
data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }

(emphasis on the word equivalent)

Upvotes: 4

Related Questions