2

我正在阅读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) =>）让我感到困惑。

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

4

1 回答 1

5

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

{-# 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
于 2017-09-19T16:15:20.450 回答