haskell - 我可以在运行时检查实例存在吗？

Question

我有一个有限向量的数据族:

data family Vec (n :: Nat) e
data instance Vec 2 Float = Vec2f !Float !Float
data instance Vec 3 Float = Vec3f !Float !Float !Float
-- and so on

我还有一系列 getter 函数:

class Get (i :: Nat) (n :: Nat) e where
    get :: Vec n e -> e

instance Get 0 2 Float where
    get (Vec2f x _) = x

instance Get 1 2 Float where
    get (Vec2f _ x) = x

instance Get 0 3 Float where
    get (Vec3f x _ _) = x

instance Get 1 3 Float where
    get (Vec3f _ x _) = x

instance Get 2 3 Float where
    get (Vec3f _ _ x) = x
-- and so on

这样，在编译时检查对 vector 元素的访问，因此编译:

get @0 (Vec2f 0 1)

这不是:

get @4 (Vec2f 0 1)

现在，我想知道我是否可以使用这些函数编写运行时范围检查。我试过这个:

get' :: forall n e. (KnownNat n) => Integer -> Vec n e -> Maybe e
get' i v =
    if i >= 0 && i < natVal (Proxy :: Proxy n)
        then (flip fmap) (someNatVal i) $ \(SomeNat (Proxy :: Proxy i)) ->
            get @i v -- Could not deduce (Get i n e)
        else Nothing

我想我必须在运行时检查 Get i n e 实例是否存在，有没有办法做到这一点？

Answer 1

我认为没有任何简单的方法。

Haskell 的设计使得所有类型级别的东西都可以在运行时删除。我知道的唯一方法是利用 KnownNat 和 Typeable 并手动检查每个实例。例如。像这样的东西:

get' :: forall n e. (Typeable e, KnownNat n) => Integer -> Vec n e -> Maybe e
get' 0 v =
    case sameNat (Proxy @n) (Proxy @2) of
      Just Refl -> case eqT :: Maybe (e :~: Float) of
                     Just Refl -> Just $ get @0 v
                     Nothing -> Nothing  -- TODO check for e/=Float
      Nothing -> case sameNat (Proxy @n) (Proxy @3) of
         Just Refl -> case eqT :: Maybe (e :~: Float) of
            Just Refl -> Just $ get @0 v
            Nothing -> Nothing  -- TODO check for e/=Float
         Nothing -> Nothing -- TODO check for n/=2,3
get' i v = Nothing -- TODO check for i>0

(这可能会使用一些因式分解...)

可能更好的方法是定义具体化字典的列表(或其他任何内容)，然后循环遍历它。不过，需要使此类列表与实际实例保持同步。

也许将来 Haskell 也会在运行时获得类型类搜索机制。到目前为止，这还没有完成，我猜，因为在 Haskell 中转向运行时类型级别检查是非常不合常理的。然而，在我们得到 DataKinds 和 KnownNat 以及类似的东西之后，也许静态信息在运行时的具体化/“反射”变得更有趣了。