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

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

这样,在编译时检查对向量元素的访问,因此这将编译:

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类似的东西之后,也许在运行时对静态信息的实现/"反射"变得更加有趣.