我可以在運行時檢查實例存在嗎？

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 

我也有一個家庭的吸氣劑的功能：

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以及類似的東西之後，可能在運行時對靜態信息的提取/「反射」變得更有趣。

Answer 2

現在的一個問題是Get的實例都是特設的，所以很難提供一個乾淨的解決方案。如果你願意重構Get了一下，就簡單多了：

class Get (n :: Nat) e where 
    get :: (KnownNat i, i <= (n-1)) => Proxy i -> Vec n e -> e 

instance Get 2 Float where 
    get :: (KnownNat i, i <= 1) => Proxy i -> Vec 2 Float -> Float 
    get p (Vec2f x y) = case natVal p of 
     0 -> x 
     1 -> y 
     _ -> error ":(" 

然後，你可以做

get' :: forall n e. (Get n e, KnownNat (n - 1)) => Integer -> Vec n e -> Maybe e 
get' i v = do 
    -- bring KnownNat i into context 
    SomeNat (iProx@Proxy) <- someNatVal i   -- will be Nothing if i < 0 
    -- bring i <= (n - 1) into context 
    Refl   <- iProx `isLE` (Proxy @(n - 1)) -- will be Nothing if i >= n 
    return (get iProx v) 

從typelits-證人庫帶來的不等式約束到右鍵使用GHC.TypeLits.Compare供GHC使用。