Могу ли я проверить присутствие экземпляра во время выполнения?

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 и подобные материалы, возможно, еще более интересным было reification/«отражение» статической информации во время выполнения.

Answer 2

Одна проблема прямо сейчас состоит в том, что экземпляры Get - это все виды ad-hoc, поэтому трудно обеспечить чистое решение. Если вы готовы реорганизовать 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) 

Использование GHC.TypeLits.Compare из typelits свидетелей библиотеки принести неравенство ограничение в контексте для использования GHC.