How can I avoid multiple function implementations with GADTs?

Question

First of all, here is a minimum example of my code:

{-# LANGUAGE GADTs #-}

-- package "url"
import Network.URL (exportURL, URL(..), URLType(..))

data MyURL a where
    GalleryURL :: URL -> MyURL URL
    PictureURL :: URL -> MyURL URL

url = URL { url_type = PathRelative, 
            url_path = "www.google.com", 
            url_params = []}

galleryURL = GalleryURL url

myExportURL :: MyURL a -> String
myExportURL (GalleryURL a) = exportURL a
myExportURL (PictureURL a) = exportURL a

main = print $ myExportURL galleryURL

I use GADTs to avoid mixing different kinds of URLs. The myExportURL function is the same for all kinds of URLs. Is there a way to use something like this:

myExportURL (_ a) = exportURL a

instead of repeating it for every subtype (what is the correct term?) of the GADT?

Any other comments on the code or the problem i am trying to solve are also welcome.

Answer 1

The correct term is "for every constructor".

Your GADT look suspicious as all your constructors construct the same MyURL URL type. If it's all you want then you don't need GADTs in the first place and can use plain ADTs:

data MyURL = GalleryURL URL | PictureURL URL

To have shorter myExportUrl there are different options. One is to refactor the type:

data URLKind = GalleryURL | PictureURL
data MyURL = MyURL { myUrlKind :: URLKind, myExportURL :: URL }

This way you can still use "short" form of construction, e.g. MyURL PictureURL foo. And also you can use myExportURL function generated for you by Haskell.

GADTs are only necessary in advanced cases so if your example does not demonstrate fully why you need GADTs then let us now.

Answer 2

Your MyURL type doesn't prevent you from mixing gallery and picture URLs. Both a GalleryURL and a PictureURL have the same type, MyURL URL. Try something like this instead:

data Gallery = Gallery

data Picture = Picture

data MyURL a where
    MyURL :: a -> URL -> MyURL a

Then you can write the remainder of your code like you imagined:

url = URL { url_type = PathRelative, 
            url_path = "www.google.com", 
            url_params = []}

galleryURL = MyURL Gallery url

myExportURL :: MyURL a -> String
myExportURL (MyURL _ a) = exportURL a

main = print $ myExportURL galleryURL

You don't need a GADT when all of the constructors work for all of the types, and you don't really need constructors for the Gallery and Picture types, so you could write these parts as:

data Gallery -- requires the empty type extension
data Picture
data MyURL a = MyURL URL

galleryURL :: MyURL Gallery
galleryURL = MyURL url

myExportURL :: MyURL a -> String
myExportURL (MyURL a) = exportURL a

Answer 3

Others have suggested modifying the data structure, here is a different approach using pattern synonyms:

{-# Language GADTs, PatternSynonyms, ViewPatterns, TypeOperators #-}

import Data.Kind

data MyURL a where
  GalleryURL :: URL -> MyURL URL
  PictureURL :: URL -> MyURL URL

url :: MyURL a -> URL
url (GalleryURL u) = u   --  Proof that: URL ~ a
url (PictureURL u) = u   --  Proof that: URL ~ a

-- Works on ‘MyURL a’ for any ‘a’
pattern Url :: URL -> MyURL a 
pattern Url u <- (url -> u)

Should another constructor be added that does not contain a URL we must add a failure case for url

data MyURL a where
  GalleryURL :: URL -> MyURL URL
  PictureURL :: URL -> MyURL URL
  I          :: Int -> MyURL Int

url :: MyURL a -> Maybe URL
url (GalleryURL u) = Just u    --  Proof that: URL ~ a
url (PictureURL u) = Just u    --  Proof that: URL ~ a
url (I i)          = Nothing   --  Proof that: Int ~ a

pattern Url :: URL -> MyURL a 
pattern Url u <- (url -> Just u)

showMyURL :: MyURL a -> String
showMyURL (Url u) = show u
showMyURL (I   i) = show i   --  Proof that: Int ~ a

Yet! — Let's say that we want an evaluation function that returns an a when given MyURL a — this works as intended

eval :: MyURL a -> a
eval (GalleryURL url) = url   --  Proof that: URL ~ a
eval (PictureURL url) = url   --  Proof that: URL ~ a
eval (I int)          = int   --  Proof that: Int ~ a

but our new Url pattern synonym fails!

eval :: MyURL a -> a
eval (Url url) = url    

We get no new information about a when we pattern match on the pattern synonym

pattern Url :: URL -> MyURL a

the connection between a and URL has been severed. We import Data.Type.Equality and add a proof Refl :: a :~: URL that a equals URL:

-- Gets ‘URL’ from a ‘MyURL URL’
--
-- ‘Refl’ is our proof that the input is ‘MyURL URL’ 
url :: MyURL a -> Maybe (a :~: URL, a)
url (GalleryURL url) = Just (Refl, url)
url (PictureURL url) = Just (Refl, url)
url (I          int) = Nothing

Then we say that Url _ provides a proof that a ~ URL when matched against,

pattern Url :: () => a ~ URL => a -> MyURL a
pattern Url url <- (Url -> (Refl, url))

and the URL can again be retrieved with a single pattern

eval :: MyURL a -> a
eval (Url url) = url   --  Proof that: URL ~ a
eval (I   int) = int   --  Proof that: Int ~ a