我可以用推广类型进行分支控制吗？

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)

但在这种情况下,我不确定有多重要.

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

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

这使得单例在某些情况下更加隐含.

希望Richard Eisenberg将DependentHaskell在未来几年内完成他的工作,此时所有这些都将变得更加痛苦.