如何从具有类型相等约束的 Scott 编码的 GADT 中获取值？

Question

我正在阅读24 天 GHC 扩展的 Rank-N-Types 部分并遇到以下 GADT：

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}

import Data.Char

data Some :: * -> * where
    SomeInt  :: Int -> Some Int
    SomeChar :: Char -> Some Char
    Anything :: a -> Some a

unSome :: Some a -> a
unSome (SomeInt x) = x + 3
unSome (SomeChar c) = toLower c
unSome (Anything x) = x

unSome (someInt 2) -- 5

尽管unSome它的类型变量是多态的，但可以向编译器证明在这种SomeInt情况下，将三个添加到给定值是安全的。作者将这种类型称为细化。

现在我很好奇我是否可以用 Scrott 编码类型做同样的事情。幸运的是，有一个这种编码的例子。我们只需要打开 Rank-N-Types 和 Type-Families 扩展：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

newtype SomeC a =
    SomeC {
      runSomeC ::
          forall r.
          ((a ~ Int) => Int -> r) ->
          ((a ~ Char) => Char -> r) ->
          (a -> r) ->
          r
    }

但是，unSome在文章中没有提供。我不精通 Haskell，也不知道如何使用 Scott 编码实现此功能。尤其是类型相等约束（例如(a ~ Int) =>）让我感到困惑。

感谢有关其他在线资源的任何帮助或信息。

Answer 1

您只需使用提供的函数来替换您的模式匹配，如下所示：

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}

import Data.Char

newtype SomeC a =
    SomeC {
      runSomeC ::
          forall r.
          ((a ~ Int) => Int -> r) ->
          ((a ~ Char) => Char -> r) ->
          (a -> r) ->
          r
    }

unSome :: SomeC a -> a
unSome (SomeC f) = f (\x -> x+3) (\c -> toLower c) (\x -> x)

在ghci中：

> unSome (SomeC (\someInt someChar anything -> someInt 2))
5