haskell - Convert Sum Type to Phantom Type via Type Classes

Question

I was experimenting with phantom types in Haskell. My goal is to convert the LangCode Type to it's corresponding Phantom Type representation via Type Classes for example DE to 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

With a type annotation it works fine. But without it I get this error.

[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

My question is. Is it possible to implement it in a way so that the type annotations are no longer needed?

Updated version

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

Answer 1

这就是问题所在。这是类型的基本属性，如果术语级表达式e1和e2具有相同的 type t，那么在程序中替换e1withe2不会改变程序的任何类型。这就是他们类型的原因。

您想要表达式（没有明确的类型签名）：

fromLangCode EN

有 type Lang EN，这很容易。但是，如果术语级表达式EN和DE是来自相同总和类型的构造函数LangCode，那么用一个替换另一个不会改变任何类型，所以表达式：

fromLangCode DE

仍然会有type Lang EN，这显然不是你想要的。

所以，如果你想要两种不同的推断类型：

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

那么任何解决方案都将要求术语级表达式EN并DE具有不同的类型，这意味着您不能拥有：

data LangCode = EN | DE

所以，这就是简短的答案——您不能LangCode在 sum 类型和 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

一切都或多或少像我之前的示例一样，对类型签名进行了一些小的更改，并且main保持不变，如下所示：

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

因此，我们可以在这种广义求和类型和幻象类型表示之间自由转换。

与前面的示例相比，这确实不是很大的改进。这两个构造函数现在正式成为广义 sum 类型的一部分，但是术语级别的表达式在类型级别EN上DE已经不同了，我们只是在一种类型级别表示（类型LangCode EN和LangCode DE）和另一种（类型Lang EN和Lang DE）之间转换.

但是，您的“更新示例”可能会受到同样的批评。通过引入单例（一种广义的 sum 类型），您也已经在第一个单例参数的类型级别上创建了表达式fromLangCode SDE DE和不同的表达式。fromLangCode SEN EN第二个，术语级别的参数在这里没有用处，可以被消除，所以你只是从一种类型级别的表示（SLangCode DEvs SLangCode EN）转换为另一种（Lang DEvs Lang EN）。

存在类型

术语和类型级别表示之间的实际有用转换通常涉及混合中某处的存在类型。考虑一个更现实的例子会有所帮助。假设您可能希望能够使用类型系统来帮助避免不恰当地混合语言。例如：

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

但是，您可能还想在运行时决定在特定表达式中使用哪种语言：

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

这不起作用，因为类型mytext不能依赖于运行时计算。也就是说，没有简单的方法可以将运行时术语级别的值language :: LangCode（求和类型）转换为类型级别的值Lang language，即所需的mytext.

通常的解决方案是使用存在类型：

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

这里，类型SomeText表示某种未指定语言的文本（即，Text lang某个未指定类型的类型值lang）。现在，mytext可以通过用SomeText构造函数包装文本来以运行时确定的语言分配文本。

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

我们只能用一个SomeText价值来做有限的事情mytext——我们不能做任何依赖于了解语言的事情，比如申请pluralize等等fixß。但是，我们可以做的一件事是提取字符串，因为它适用于任何语言：

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

这使我们可以编写一个有用的main：

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

这是完整的工作示例：

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

我们在这里所做的是成功地将术语级别的值从 sum 类型 ( language) 转换为类型级别的值Text language，方法是将其包装在SomeText构造函数中。

应用于您的示例

我们可以使用相同的技术在 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>