对现有数据类型强制使用类型类型约束

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 -> (可键入a => r) -> r

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

1. 升级Sing实例。写

data STypeable a where STypeable :：type a => SType a -> STypeable a type实例Sing = STypeable

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

可能还有其他方法。

Answer 2

您可以完全避免CPS风格。每当我看到(Cls a => res) -> res时，我更喜欢使用模式匹配。

单件有pattern FromSing，它用模式匹配代替withSomeSing：

checkResult :: EType -> UntypedExp -> Maybe Result
checkResult (FromSing (singType :: SType a)) expr = ..

然后定义一种从Typeable获取SType约束的方法。出于这些目的，您可以在类型索引的TypeRep上匹配来自Type.Reflection的模式。最近添加了pattern FromSing和pattern TypeRep，以免与TypeRep类型构造函数混淆，因此请检查是否有最新版本。

pattern STypeRep :: () => Typeable a => SType a
pattern STypeRep <- (stypeRep -> TypeRep)
--where STypeRep = stype typeRep

stypeRep :: SType a -> TypeRep a
stypeRep = \case
 SInteger -> typeRep
 SBoolean -> typeRep
 SByteStr -> typeRep

-- optional and partial actually
-- stype :: forall a. TypeRep a -> SType a
-- stype rep
--   | Just HRefl <- eqTypeRep rep (typeRep @Int)
--   = SInteger
--   | Just HRefl <- eqTypeRep rep (typeRep @Bool)
--   = SBoolean
--   | Just HRefl <- eqTypeRep rep (typeRep @ByteString)
--   = SByteStr
--   | let
--   = error "crash and burn"

最后表格：

checkResult :: EType -> UntypedExp -> Maybe Result
checkResult (FromSing singType@STypeRep) = fmap (makeResult singType) . inferExpr