Как можно избежать нескольких реализаций функций с помощью GADT?

Question

Прежде всего, вот минимальный пример моего кода:

{-# 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

Я использую GADT, чтобы избежать смешивания разных типов URL. myExportURL Функция одинакова для всех видов URL. Есть ли способ использовать что-то вроде этого:

myExportURL (_ a) = exportURL a

вместо того, чтобы повторять это для каждого подтипа (каков правильный термин?) GADT?

Любые другие комментарии по коду или проблеме, которую я пытаюсь решить, также приветствуются.

Answer 1

Правильный термин "для каждого конструктора".

Ваш GADT выглядит подозрительно, так как все ваши конструкторы строят одинаково MyURL URL тип. Если это все, что вам нужно, вам не нужны GADT, и вы можете использовать простые ADT:

data MyURL = GalleryURL URL | PictureURL URL

Короче myExportUrl Есть разные варианты. Одним из них является рефакторинг типа:

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

Таким образом, вы все еще можете использовать "короткую" форму конструкции, например MyURL PictureURL foo, А также вы можете использовать myExportURL функция, сгенерированная для вас Haskell.

GADT необходимы только в сложных случаях, поэтому, если ваш пример не полностью демонстрирует, зачем вам нужны GADT, сообщите нам об этом.

Answer 2

Ваш тип MyURL не мешает вам смешивать URL галереи и изображения. И GalleryURL, и PictureURL имеют одинаковый тип, MyURL URL, Попробуйте что-то вроде этого:

data Gallery = Gallery

data Picture = Picture

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

Затем вы можете написать оставшуюся часть кода, как вы себе представляли:

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

Вам не нужен GADT, когда все конструкторы работают для всех типов, и вам не нужны конструкторы для типов Gallery и Picture, поэтому вы можете написать эти части следующим образом:

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

Другие предложили изменить структуру данных, здесь используется другой подход с использованием синонимов шаблонов:

{-# 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)

Если будет добавлен другой конструктор, который не содержит URL мы должны добавить случай отказа для 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

Еще! - Допустим, мы хотим функцию оценки, которая возвращает a когда дано MyURL a - это работает как задумано

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

но наш новый Url синоним шаблона не работает!

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

Мы не получаем никакой новой информации о a когда мы сопоставляем образец по синониму образца

pattern Url :: URL -> MyURL a

связь между a а также URL был разорван. Мы импортируем Data.Type.Equality и добавляем доказательство Refl :: a :~: URL тот a равняется 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

Тогда мы говорим, что Url _ обеспечивает доказательство того, что a ~ URL когда сопоставлено,

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

и URL можно снова получить с помощью одного шаблона

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