haskell - 对现有数据类型实现类型类约束

Question

也许有更好的方法来实现我想要的，但这是我目前的尝试。

我正在使用 singletons打包以便将值具体化为类型。这工作正常，但在某些时候我将不得不运行一个在具体化类型 中是多态的函数，并期望它有一个 Typeable 实例。当然，Haskell 中的所有类型都有这样的实例(至少 afaik？)，但是由于类型变量在编译时是未知的，所以类型检查器无法找到这样的实例。让我举例说明:

{-# LANGUAGE GADTs, FlexibleInstances, RankNTypes, PolyKinds, TypeFamilyDependencies, InstanceSigs #-}

import Data.ByteString (ByteString)
import Data.Typeable (Typeable)
import Data.Singletons

-- The unreified type.
data EType
  = Integer
  | Boolean
  | ByteStr
  deriving (Eq, Ord, Show, Read)

-- The corresponding singleton types.
-- Note that the parameter piggybacks
-- on Haskell's regular types.
data SType a where
  SInteger :: SType Int
  SBoolean :: SType Bool
  SByteStr :: SType ByteString

-- My singleton types are singletons.
type instance Sing = SType

-- Makes it possible to reify `EType` into `Int`,
-- `Bool` and `ByteString`, and to reflect back
-- from them to `EType`.
instance SingKind * where
  type Demote * = EType
           
           -- SType a       -> EType 
  fromSing :: Sing (a :: *) -> Demote *
  fromSing SInteger = Integer
  fromSing SBoolean = Boolean
  fromSing SByteStr = ByteStr

         -- EType    -> SomeSing *
  toSing :: Demote * -> SomeSing *
  toSing Integer = SomeSing SInteger
  toSing Boolean = SomeSing SBoolean
  toSing ByteStr = SomeSing SByteStr

-- Some dummy types for illustration.
-- Should be self-explanatory.
data UntypedExp
data Exp a
data Result

-- The function I actually want to implement.
checkResult :: EType -> UntypedExp -> Maybe Result
checkResult typ expr = withSomeSing typ $ \singType ->
  makeResult singType <$> inferExpr expr

-- A version of my main type checking function (some 
-- inputs omitted). The caller chooses `a`, and
-- depending on whether the input can be typed in
-- that way or not, we return `Just e` or `Nothing`.
-- THIS IS ALREADY IMPLEMENTED.
inferExpr :: Typeable a => UntypedExp -> Maybe (Exp a)
inferExpr = undefined

-- Depending on `a`, this function needs to do
-- different things to construct a `Result`.
-- Hence the reification.
-- THIS IS ALREADY IMPLEMENTED.
makeResult :: Sing a -> Exp a -> Result
makeResult = undefined

这给了我错误

    • No instance for (Typeable a) arising from a use of ‘inferExpr’
    • In the second argument of ‘(<$>)’, namely ‘inferExpr expr’
      In the expression: makeResult singType <$> inferExpr expr
      In the second argument of ‘($)’, namely
        ‘\ singType -> makeResult singType <$> inferExpr expr’
   |
54 |   makeResult singType <$> inferExpr expr
   |                           ^^^^^^^^^^^^^^

这很有道理。 withSomeSing 不保证传递给延续的 Sing a 满足 Typeable a。

我可以解决这个问题，方法是隐藏一些来自 Data.Singleton 的导入，而不是使用相关约束定义我自己的版本:

import Data.Singletons hiding (SomeSing,SingKind(..),withSomeSing)

withSomeSing :: forall k r
              . SingKind k
             => Demote k                          
             -> (forall (a :: k). Typeable a => Sing a -> r)
             -> r
withSomeSing x f =
  case toSing x of
    SomeSing x' -> f x'

class SingKind k where
  type Demote k = (r :: *) | r -> k
  fromSing :: Sing (a :: k) -> Demote k
  toSing   :: Demote k -> SomeSing k

data SomeSing k where
  SomeSing :: Typeable a => Sing (a :: k) -> SomeSing k

这使一切正常，但感觉绝对是糟糕的风格。

因此我的问题是:是否有任何方法可以导入 SomeSing 和 withSomeSing 的原始定义，但使用此附加约束来扩充它们的类型？或者，您建议如何以更好的方式解决这个问题？

Answer 1

我想到了两个选项:

1. 实现

    withTypeable :: SType a -> (Typeable a => r) -> r
   

   通过对第一个参数进行详尽的模式匹配。然后，您不仅可以使用 withSomeSing，还可以同时使用两者，如 withSomeSing typ $\singType -> withTypeable singType $ ...。

2. 升级您的 Sing 实例。写

    data STypeable a where STypeable :: Typeable a => SType a -> STypeable a
    type instance Sing = STypeable
   

   您需要在 toSing 和 fromSing 的每个分支中添加一个额外的 STypeable 构造函数。然后您可以在 withSomeSing 中进行模式匹配，如 withSomeSing $\(STypeable singType) -> ...。

可能还有其他方法。