2

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

我正在使用该singletons包以将值具体化为类型。这很好用，但在某些时候，我将不得不运行一个在具体类型中具有多态性的函数，并期望它有一个Typeableinstance。当然，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传递给 continuation 满足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

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

因此我的问题是：有什么方法可以导入 and 的原始定义SomeSing，withSomeSing但是用这个额外的约束来增加它们的类型？或者，您如何建议以更好的方式解决这个问题？

4

2 回答 2

4

两个选项浮现在脑海：

  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

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

可能还有其他方法。

于 2021-09-09T19:07:30.480 回答
2

您可以完全避免 CPS 风格。任何时候我看到(Cls a => res) -> res我都喜欢使用模式匹配。

单例有模式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
于 2021-09-10T16:32:50.183 回答