Как я могу избежать реализации нескольких функций с помощью 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 

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

myExportURL (_ a) = exportURL a 

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

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

Answer 1

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

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

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 

Yet! - Давайте предположим, что мы хотим оценочную функцию, которая возвращает 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