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

Question

我正在阅读 the Rank-N-Types section of 24 days of GHC Extensions并遇到了以下 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