haskell - 让函数根据参数的值返回不同的类型

Question

给定这个接口(interface):

{-# LANGUAGE DataKinds      #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies   #-}
module Tlf where

import           Data.Dynamic  (Dynamic, fromDyn, toDyn)
import           Data.Kind     (Type)
import           Data.Proxy    (Proxy (Proxy))
import           Data.Typeable (Typeable)

data Q = Q1 | Q2
       deriving (Show)

data R1 = R1 deriving (Show)
data R2 = R2 deriving (Show)

newtype TL (a :: [Type]) = TL { unTL :: Dynamic }

someFun :: Q -> TL '[R1, R2]
someFun Q1 = (TL . toDyn) R1
someFun Q2 = (TL . toDyn) R2

我想写一个运行 someFunc的函数并提取返回值。这有效:

myQ :: (Typeable a) => Proxy a -> Q -> a
myQ _ q = (fromDyn . unTL . someFun) q (error "This shouldn't happen!")

> myQ (Proxy :: Proxy R1) Q1
R1

但是额外的 Proxy是多余的，它并不像它应该的那样安全

*Tlf> myQ (Proxy :: Proxy R2) Q1
*** Exception: This shouldn't happen!

问题是我知道 Q1将产生 R1 .所以我写了这个:

type family FunRes (a :: Q) :: Type where
  FunRes 'Q1 = R1
  FunRes 'Q2 = R2

但现在我被困在如何将这些碎片组合在一起。我试过:

myQ' :: forall q. q -> FunRes q
myQ' q = (fromDyn . unTL . someFun) q (error "This shouldn't happen!")

但是 ghc 说不:

    • Expected kind ‘Q’, but ‘q’ has kind ‘*’
    • In the first argument of ‘FunRes’, namely ‘q’
      In the type signature: myQ' :: forall q. q -> FunRes q

我还尝试了其他一些事情，但我总是偶然发现上面给出的错误。

Answer 1

问题是，你试图让 myQ根据参数的值返回不同的类型(编辑:当我写这个时，问题有不同的标题)。这不可能发生。 Haskell 就是不支持这种事情。
(如果您想查找并研究更多，这称为“依赖类型” - 因为类型取决于值)
在 Haskell 中，您可以执行某些折中的措施。例如，一种流行的方法称为“singleton”，在这种方法中，您将自己设置为带有 Q 值标记的案例的 GADT。提升为类型:

data SQ (q :: Q) where
  SQ1 :: SQ Q1
  SQ2 :: SQ Q2

然后你创建一个函数来转换 SQ至 Q :

reflectQ :: SQ q -> Q
reflectQ SQ1 = Q1
reflectQ SQ2 = Q2

然后 myQ可以变成:

myQ :: Typeable (FunRes q) => SQ q -> FunRes q
myQ q = (fromDyn . unTL . someFun) (reflectQ q) (error "This shouldn't happen!")

你会这样称呼它:

> myQ SQ1
R1

> myQ SQ2
R2

但这有一个明显的问题:你只能通过 SQ1和 SQ2在编译时。例如，它们不能来自用户输入。
或者，更准确地说，他们可以，但你又回到不知道结果的类型。它必须保持通用。就像我在顶部所说的那样，Haskell 最终不支持依赖类型。

另外，如果你足够用力地眯着眼睛，你可以看到 R1和 R2已经有点扮演 SQ1的角色了和 SQ2 ，所以你不妨这样做:

class RtoQ r where reflectRtoQ :: Q
instance RtoQ R1 where reflectRtoQ = Q1
instance RtoQ R2 where reflectRtoQ = Q2

myQ :: forall a. (Typeable a, RtoQ a) => a
myQ = (fromDyn . unTL . someFun) (reflectRtoQ @a) (error "This shouldn't happen!")

> myQ @R1
R1

> myQ @R2
R2

这比“单例”方法稍差，因为 SQ 的值可以传递，存储在数据结构中，以及您可以对值执行的所有其他操作，而类型 R1和 R2不能。