haskell - 我可以使用提升类型进行分支控制吗？

Question

我创建了一个玩具程序来尝试在升级类型上进行分支:

{-# LANGUAGE KindSignatures, DataKinds, TypeFamilies, ScopedTypeVariables, GADTs #-}
module Foo where

import Data.Proxy

data Out = ToInt | ToBool

type family F (a :: Out) where
    F ToInt = Int
    F ToBool = Bool

foo :: forall k. Proxy (k :: Out) -> Int -> F k
foo p = case p of
    (Proxy :: Proxy 'ToInt) -> id
    (Proxy :: Proxy 'ToBool) -> (== 0)

在这里，我尝试在 Proxy 上分支并在它们上使用显式类型签名，但这不起作用，GHC 提示:

[1 of 1] Compiling Foo              ( Foo.hs, Foo.o )

Foo.hs:15:6: error:
    • Couldn't match type ‘k’ with ‘'ToBool’
      ‘k’ is a rigid type variable bound by
        the type signature for:
          foo :: forall (k :: Out). Proxy k -> Int -> F k
        at Foo.hs:12:15
      Expected type: Proxy 'ToBool
        Actual type: Proxy k
    • When checking that the pattern signature: Proxy 'ToBool
        fits the type of its context: Proxy k
      In the pattern: Proxy :: Proxy ToBool
      In a case alternative: (Proxy :: Proxy ToBool) -> (== 0)
    • Relevant bindings include
        p :: Proxy k (bound at Foo.hs:13:5)
        foo :: Proxy k -> Int -> F k (bound at Foo.hs:13:1)

我认为这基本上表明 GHC 无法计算出第二个分支上的 k ~ 'ToBool 。 (实际上第一个分支对于非常相似的错误消息也不起作用)

这实际上可能吗，还是我做错了什么？

Answer 1

这是不可能的。类型会被删除，因此您无法在运行时直接使用它们来做出决策。通常的做法是用单例替换代理。在这种情况下，我认为类型族太过分了，所以我放弃了它。

data Out a where
  ToInt :: Out Int
  ToBool :: Out Bool

foo :: forall k. Out k -> Int -> k
foo p = case p of
    ToInt -> id
    ToBool -> (== 0)

如果您愿意，您可以使用 DataKinds 来提升您的 Out 构造函数并通过以下方式索引单例类型:

data OutS a where
  ToIntS :: OutS 'ToInt
  ToBoolS :: OutS 'ToBool

foo :: forall k. OutS k -> Int -> F k
foo p = case p of
   ToIntS -> id
   ToBoolS -> (== 0)

但在这种情况下，我不确定这有什么意义。

另一个设计选项(您可以与上述任一选项一起使用)是使用类将类型与其单例绑定(bind):

class SConv t where
  sConv :: proxy t -> OutS t
instance SConv 'ToInt where
  sConv _ = ToIntS
instance SConv 'ToBool where
  sConv _ = ToBoolS

这使得单例传递在某些情况下更加隐式。

希望 Richard Eisenberg 能够在未来几年内完成他的 DependentHaskell 工作，届时这一切都会变得不那么痛苦。