是否可以将值提升到类型级别？

问题描述

这样做只是为了好玩，但我最终没有弄清楚。

假设我有一个统一正方形和六边形坐标系的类型类：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

import Data.Proxy

data Shape = Square | Hexagon

class CoordSystem (k :: Shape) where
  type Coord k

  -- all coordinates arranged in a 2D list
  -- given a side length of the shape
  allCoords :: forall p. p k -> Int -> [[Coord k]]

  -- neighborhoods of a coordinate.
  neighborsOf :: forall p. p k -> Int -> Coord k -> [Coord k]

-- omitting implementations
instance CoordSystem 'Square
instance CoordSystem 'Hexagon

现在假设我想将此接口与仅在运行时已知的 s :: Shape 一起使用。但是为了使用这个接口，在某些时候我需要一个像这样的函数：

-- none of those two works:
-- promote :: CoordSystem k => Shape -> Proxy (k :: Shape) -- signature 1
-- promote :: Shape -> forall k. CoordSystem k => Proxy (k :: Shape)

promote s = case s of
  Square -> Proxy @'Square
  Hexagon -> Proxy @'Hexagon

但是，如果未注释签名 1，这将不起作用：

    • Couldn't match type ‘k’ with ‘'Square’
      ‘k’ is a rigid type variable bound by
        the type signature for:
          promote :: forall (k :: Shape). CoordSystem k => Shape -> Proxy k
        at SO.hs:28:1-55
      Expected type: Proxy k
        Actual type: Proxy 'Square

可以理解，'Square、'Hexagon、k :: Shape 都没有与其他人统一，所以我不知道这是否可能。

我也觉得类型擦除在这里不应该成为问题，因为 Shape 的替代品可以用来唯一标识实例 - 因此我觉得 singletons 可能有用，但我不是熟悉该包以生成任何工作示例。

解决方法

通常的方法是使用存在类型或其 Church 编码。我认为，编码版本一开始实际上更容易理解，并且更接近您已经尝试过的内容。您的 forall k. CoordSystem k => {- ... thing mentioning k -} 的问题在于它承诺将变形为用户喜欢的任何 k（只要用户喜欢 CoordSystem！）。要解决这个问题，您可以要求 user 变身为 k 您喜欢的任何东西。

                              -- `a` must not mention `k`,since `k` is not
                              -- in scope in the final return type
promote :: forall a. Shape -> (forall k. CoordSystem k => Tagged k a) -> a
promote Square a = unTagged (a @Square)
promote Hexagon a = unTagged (a @Hexagon)

-- usage example
test = promote Hexagon (unproxy $ \p -> length (allCoords p 15))

请注意，在 = 符号的右侧，a 的类型为 forall k. CoordSystem k => {- ... -}，表示用户可以选择 k，但这次您重新回到用户。

另一个常见的选择是使用一个存在：

data SomeSystem where
    -- Proxy to be able to name the wrapped type when matching on a SomeSystem;
    -- in some future version of GHC we may be able to name it via pattern-matching
    -- on a type application instead,which would be better
    SomeSystem :: CoordSystem k => Proxy k -> SomeSystem

然后你会写一些类似的东西

promote :: Shape -> SomeSystem
promote Square = SomeSystem (Proxy @Square)
promote Hexagon = SomeSystem (Proxy @Hexagon)

-- usage example
test = case promote Hexagon of SomeSystem p -> length (allCoords p 15)

然后用户将进行模式匹配以从中提取 CoordSystem 实例。

最后的选择是单例：

data ShapeS k where
    SquareS :: ShapeS Square
    HexagonS :: ShapeS Hexagon

这里我们在计算级别的 SquareS 和类型级别的 Square 之间建立了直接联系（分别是 HexagonS 和 Hexagon）。然后你可以写：

                       -- N.B. not a rank-2 type,and in particular `a` is
                       -- now allowed to mention `k`
promote :: ShapeS k -> (CoordSystem k => a) -> a
promote SquareS a = a
promote HexagonS a = a

singletons 包提供了用于自动派生与您的 ADT 对应的单例类型的工具。

data-kinds haskell haskell