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

異なる種類の URL が混在しないように、GADT を使用しています。このmyExportURL機能は、すべての種類の URL で同じです。このようなものを使用する方法はありますか：

myExportURL (_ a) = exportURL a

GADT のすべてのサブタイプ (正しい用語は?) ごとに繰り返す代わりに?

コードまたは私が解決しようとしている問題に関するその他のコメントも大歓迎です。

4

3 に答える 3

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)

を含まない別のコンストラクターを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を追加します。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 に答える