通過型別類將Sum型別轉換為Phantom型別-有解無憂

我在 Haskell 中試驗幻像型別。我的目標是LangCode通過 Type Classes將Type轉換為它對應的 Phantom Type 表示，例如DEto Lang DE.

module Main (main) where

import Data.Proxy (Proxy(..))

data DE
data EN

data LangCode
  = DE
  | EN
  deriving (Eq, Show)

type Lang a = Proxy a

de :: Lang DE
de = Proxy

en :: Lang EN
en = Proxy

class ToLangCode a where
  toLangCode :: Lang a -> LangCode

instance ToLangCode DE where
  toLangCode _ = DE
instance ToLangCode EN where
  toLangCode _ = EN

class FromLangCode a where
  fromLangCode :: LangCode -> Lang a

instance FromLangCode DE where
  fromLangCode DE = Proxy
instance FromLangCode EN where
  fromLangCode EN = Proxy

main :: IO ()
main = do
  print $ de -- Output => Proxy
  print $ en -- Output => Proxy

  print $ toLangCode de -- Output => DE
  print $ toLangCode en -- Output => EN

  -- works
  print $ (fromLangCode DE :: Lang DE) -- Output => Proxy
  print $ (fromLangCode EN :: Lang EN) -- Output => Proxy

  -- throws an error
  print $ fromLangCode DE -- Output => Proxy
  print $ fromLangCode EN -- Output => Proxy

使用型別注釋它可以正常作業。但沒有它我會收到這個錯誤。

[1 of 1] Compiling Main             ( main.hs, main.o )

main.hs:50:11: error:
    * Ambiguous type variable `a0' arising from a use of `fromLangCode'
      prevents the constraint `(FromLangCode a0)' from being solved.
      Probable fix: use a type annotation to specify what `a0' should be.
      These potential instances exist:
        instance FromLangCode DE -- Defined at main.hs:32:10
        instance FromLangCode EN -- Defined at main.hs:34:10
    * In the second argument of `($)', namely `fromLangCode DE'
      In a stmt of a 'do' block: print $ fromLangCode DE
      In the expression:
        do print $ de
           print $ en
           print $ toLangCode de
           print $ toLangCode en
           ....
   |
50 |   print $ fromLangCode DE -- Output => Proxy
   |           ^^^^^^^^^^^^^^^

main.hs:51:11: error:
    * Ambiguous type variable `a1' arising from a use of `fromLangCode'
      prevents the constraint `(FromLangCode a1)' from being solved.
      Probable fix: use a type annotation to specify what `a1' should be.
      These potential instances exist:
        instance FromLangCode DE -- Defined at main.hs:32:10
        instance FromLangCode EN -- Defined at main.hs:34:10
    * In the second argument of `($)', namely `fromLangCode EN'
      In a stmt of a 'do' block: print $ fromLangCode EN
      In the expression:
        do print $ de
           print $ en
           print $ toLangCode de
           print $ toLangCode en
           ....
   |
51 |   print $ fromLangCode EN -- Output => Proxy
   |           ^^^^^^^^^^^^^^^
exit status 1

我的問題是。是否有可能以一種不再需要型別注釋的方式實作它？

更新后的版本

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE FlexibleInstances #-}

module Main (main) where

data LangCode = DE | EN deriving (Eq, Show)

data SLangCode a where
    SDE :: SLangCode DE
    SEN :: SLangCode EN

data Lang (a :: LangCode) where
  LangDE :: Lang 'DE
  LangEN :: Lang 'EN

deriving instance Show (Lang 'DE)
deriving instance Show (Lang 'EN)

slcDE :: SLangCode a -> Lang 'DE -> Lang a
slcDE SDE t = t
slcDE SEN _ = LangEN

slcEN :: SLangCode a -> Lang 'EN -> Lang a
slcEN SEN t = t
slcEN SDE _ = LangDE

class ToLangCode a where
  toLangCode :: Lang a -> LangCode

instance ToLangCode 'DE where
  toLangCode _ = DE
instance ToLangCode 'EN where
  toLangCode _ = EN

class FromLangCode a where
  fromLangCode :: SLangCode a -> LangCode -> Lang a

instance FromLangCode 'DE where
  fromLangCode SDE DE = LangDE
instance FromLangCode 'EN where
  fromLangCode SEN EN = LangEN

main :: IO ()
main = do
  print $ toLangCode LangDE -- Output => DE
  print $ toLangCode LangEN -- Output => EN

  print $ fromLangCode SDE DE -- Output => LangDE
  print $ fromLangCode SEN EN -- Output => LangEN

uj5u.com熱心網友回復：

這就是問題所在。型別的一個基本屬性是，如果術語級別的運算式e1和e2具有相同的 type t，那么在程式中替換e1withe2不會改變程式的任何型別。這就是使它們型別化的原因。

你想要運算式（沒有明確的型別簽名）：

fromLangCode EN

有 type Lang EN，這很容易。但是如果術語級別的運算式EN和DE是來自相同和型別的建構式LangCode，那么用一個替換另一個不會改變任何型別，所以運算式：

fromLangCode DE

將仍然有型Lang EN，這顯然不是你想要的。

因此，如果您想要兩種不同的推斷型別：

fromLangCode EN :: Lang EN
fromLangCode DE :: Lang DE

那么任何解決方案都將要求術語級別的運算式EN并DE具有不同的型別，這意味著您不能擁有：

data LangCode = EN | DE

所以，這就是簡短的回答——您不能在 sum 型別LangCode和type 的代理之間自由轉換Lang lang。或者更確切地說，您可以使用型別類（如）輕松地從型別轉換Lang lang為術語，但您無法真正轉換回來。LangCodeToLangCode

這個“問題”有很多解決方案，但這取決于你想要做什么，這就是為什么評論中的人會問你關于“用例”和“預期行為”的問題。

一個什么都不做的簡單解決方案

一種簡單的解決方案是撰寫：

data EN = EN
data DE = DE

在這里，術語級別的運算式EN和DE具有不同的型別（EN和DE）。這使您可以使用main函式逐字輕松地實作所需的介面：

import Data.Proxy

data EN = EN deriving (Show)
data DE = DE deriving (Show)

type Lang a = Proxy a

de :: Lang DE
de = Proxy

en :: Lang EN
en = Proxy

class ToLangCode a where
  toLangCode :: Lang a -> a

instance ToLangCode DE where
  toLangCode _ = DE
instance ToLangCode EN where
  toLangCode _ = EN

class FromLangCode a where
  fromLangCode :: a -> Lang a

instance FromLangCode DE where
  fromLangCode DE = Proxy
instance FromLangCode EN where
  fromLangCode EN = Proxy

main :: IO ()
main = do
  print $ de -- Output => Proxy
  print $ en -- Output => Proxy

  print $ toLangCode de -- Output => DE
  print $ toLangCode en -- Output => EN

  -- works
  print $ (fromLangCode DE :: Lang DE) -- Output => Proxy
  print $ (fromLangCode EN :: Lang EN) -- Output => Proxy

  -- works fine now
  print $ fromLangCode DE -- Output => Proxy
  print $ fromLangCode EN -- Output => Proxy

如果你懷疑這個“解決方案”，你是對的。它并沒有真正完成任何事情，因為術語級別的運算式EN和DE在型別級別已經不同，并且該程式實際上只是在一種型別級別表示（型別EN和DE）和另一種（型別Lang EN和Lang DE）之間進行轉換。

使用 GADT

一種做你想做的事情的方法是使用 GADT。如果我們定義LangCode為“廣義”和型別：

{-# LANGUAGE GADTs #-}

data EN
data DE

data LangCode lang where
  EN :: LangCode EN
  DE :: LangCode DE

everything works more or less like my previous example, with a few minor changes to type signatures, and main left unchanged, as below:

{-# LANGUAGE GADTs #-}
{-# LANGUAGE StandaloneDeriving #-}

import Data.Proxy

data EN
data DE

data LangCode lang where
  EN :: LangCode EN
  DE :: LangCode DE
deriving instance Show (LangCode a)

type Lang a = Proxy a

de :: Lang DE
de = Proxy

en :: Lang EN
en = Proxy

class ToLangCode a where
  toLangCode :: Lang a -> LangCode a

instance ToLangCode DE where
  toLangCode _ = DE
instance ToLangCode EN where
  toLangCode _ = EN

class FromLangCode a where
  fromLangCode :: LangCode a -> Lang a

instance FromLangCode DE where
  fromLangCode DE = Proxy
instance FromLangCode EN where
  fromLangCode EN = Proxy

main :: IO ()
main = do
  print $ de -- Output => Proxy
  print $ en -- Output => Proxy

  print $ toLangCode de -- Output => DE
  print $ toLangCode en -- Output => EN

  -- works
  print $ (fromLangCode DE :: Lang DE) -- Output => Proxy
  print $ (fromLangCode EN :: Lang EN) -- Output => Proxy

  -- works fine now
  print $ fromLangCode DE -- Output => Proxy
  print $ fromLangCode EN -- Output => Proxy

So, we can freely convert between this generalized sum type and a phantom type representation.

This really isn't a big improvement over the previous example. The two constructors are now formally part of a generalized sum type, but the term-level expressions EN and DE are already distinct at the type level, and we're just converting between one type-level representation (types LangCode EN and LangCode DE) and another (types Lang EN and Lang DE).

However, the same criticism could be levelled at your "updated example". By introducing singletons (a generalized sum type), you too are already making the expressions fromLangCode SDE DE and fromLangCode SEN EN distinct at the type-level in that first, singleton argument. The second, term-level argument plays no useful role here and could be eliminated, so you're just converting from one type-level representation (SLangCode DE versus SLangCode EN) to another (Lang DE versus Lang EN).

Existental Types

Actual useful conversion between term and type-level representations usually involves an existential type somewhere in the mix. It helps to consider a slightly more realistic example. Suppose you might want to be able to use the type system to help avoid inappropriately mixing languages. For example:

import Data.List.Extra

data EN
data DE
newtype Text lang = Text String deriving (Show)

item :: Text EN
item = Text "The big elephant"

artikel :: Text DE
artikel = Text "Die gro?en Elefanten"

fix? :: Text DE -> Text DE
fix? (Text x) = Text $ replace "?" "ss" x

pluralize :: Text EN -> Text EN
pluralize (Text noun) | "s" `isSuffixOf` noun = Text $ noun    "ses"
                      | otherwise = Text $ noun    "s"

message_en :: Text EN
message_en = pluralize item

message_de :: Text DE
message_de = fix? artikel

-- type system prevents applying german manipulations to english text
type_error_1 = fix? item

But, you might also like to make a run-time decision about which language is being used in a particular expression:

data LangCode = EN | DE

main :: IO ()
main = do
  let language = EN  -- assume this comes from args or user input
  -- type error: `mytext` can't be both `Text EN` and `Text DE`
  let mytext = case language of
        EN -> message_en
        DE -> message_de
  print mytext

This doesn't work because the type of mytext can't depend on a runtime computation. That is, there's no simple way to convert the runtime term-level value language :: LangCode (a sum type) to a type-level value Lang language, the desired type of mytext.

The usual solution in is to use an existential type:

{-# LANGUAGE ExistentialQuantification #-}
data SomeText = forall lang. SomeText (Text lang)

Here, the type SomeText represents text in some unspecified language (i.e., a value of type Text lang for some unspecified type lang). Now, mytext can be assigned text in a runtime-determined language by wrapping it with the SomeText constructor.

let mytext = case language of
      EN -> SomeText message_en
      DE -> SomeText message_de

We are limited in what we can do with a SomeText value like mytext -- we can't do anything that depends on knowing the language, like applying pluralize or fix? or whatever. However, one thing we can do is extract the string, since that works for any language:

getText :: SomeText -> String
getText (SomeText (Text str)) = str

which allows us to write a useful main:

main :: IO ()
main = do
  let language = EN
  let mytext = case language of
        EN -> SomeText message_en
        DE -> SomeText message_de
  print $ getText mytext

Here's the full working example:

{-# LANGUAGE ExistentialQuantification #-}

import Data.List.Extra

data EN
data DE
data LangCode = EN | DE
newtype Text lang = Text String deriving (Show)

data SomeText = forall lang. SomeText (Text lang)

item :: Text EN
item = Text "The big elephant"

artikel :: Text DE
artikel = Text "Die gro?en Elefanten"

fix? :: Text DE -> Text DE
fix? (Text x) = Text $ replace "?" "ss" x

pluralize :: Text EN -> Text EN
pluralize (Text noun) | "s" `isSuffixOf` noun = Text $ noun    "ses"
                      | otherwise = Text $ noun    "s"

message_en :: Text EN
message_en = pluralize item

message_de :: Text DE
message_de = fix? artikel

getText :: SomeText -> String
getText (SomeText (Text str)) = str

main :: IO ()
main = do
  let language = DE
  let mytext = case language of
        EN -> SomeText message_en
        DE -> SomeText message_de
  print $ getText mytext

What we've done here is successfully converted a term-level value from a sum type (language) to a type-level value Text language by wrapping it in a SomeText constructor.

Applied to Your Example

我們可以使用相同的技術在 sum 型別和型別級別代理之間自由轉換，通過屏蔽存在型別中的型別級別代理。它可能看起來像這樣。請注意我如何使用自定義Show實體來區分不同型別的代理，以證明我們正在做一些有用的事情。

{-# LANGUAGE ExistentialQuantification #-}

import Data.Proxy

data DE
data EN

-- sum type
data LangCode
  = DE
  | EN
  deriving (Eq, Show)

-- existential for type-level proxies
type Lang = Proxy
data SomeLang = forall a. ToLangCode a => SomeLang (Lang a)
instance Show SomeLang where
  show (SomeLang lang) = "SomeLang Proxy<"    show (toLangCode' lang)    ">"

-- convert from LangCode to SomeLang
fromLangCode :: LangCode -> SomeLang
fromLangCode EN = SomeLang (Proxy :: Lang EN)
fromLangCode DE = SomeLang (Proxy :: Lang DE)

-- convert from SomeLang to LangCode
class ToLangCode lang where
  toLangCode' :: Lang lang -> LangCode
instance ToLangCode EN where
  toLangCode' Proxy = EN
instance ToLangCode DE where
  toLangCode' Proxy = DE
toLangCode :: SomeLang -> LangCode
toLangCode (SomeLang lang) = toLangCode' lang

de :: SomeLang
de = SomeLang (Proxy :: Lang DE)

en :: SomeLang
en = SomeLang (Proxy :: Lang EN)

main :: IO ()
main = do
  print $ de -- Output => SomeLang Proxy<DE>
  print $ en -- Output => SomeLang Proxy<EN>

  print $ toLangCode de -- Output => DE
  print $ toLangCode en -- Output => EN

  print $ fromLangCode DE -- Output => SomeLang Proxy<DE>
  print $ fromLangCode EN -- Output => SomeLang Proxy<EN>

轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/404604.html

標籤：

上一篇：如何僅對Haskell中的奇數索引執行某些操作？[復制]

下一篇：從Haskell中字符的字串表示創建ByteString