3

首先，这是我的代码的最小示例：

{-# 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 的每个子类型（正确的术语是什么？）重复它？

也欢迎对代码或我试图解决的问题提出任何其他意见。

4

3 回答 3

12

正确的术语是“对于每个构造函数”。

您的 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. 你也可以使用myExportURLHaskell 为你生成的函数。

GADT 仅在高级情况下是必需的，因此如果您的示例不能充分说明您需要 GADT 的原因，那么现在就让我们看看。

于 2013-08-31T13:28:19.377 回答
8

您的 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
于 2013-08-31T13:39:56.533 回答
0

其他人建议修改数据结构，这是使用模式同义词的不同方法：

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

如果添加另一个不包含 a 的构造函数，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

然而！— 假设我们想要一个在给定时返回 an 的评估函数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证明：aURL

-- 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
于 2016-11-13T22:07:36.527 回答