Kann ich die Anwesenheit von Instanzen zur Laufzeit überprüfen?

Question

Ich habe eine Daten Familie endlicher Vektoren:

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 

ich auch eine Familie von Getter Funktionen haben:

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 

Auf diese Weise Zugriff auf die Elemente eines Vektors wird zum Zeitpunkt der Kompilierung überprüft, so dies kompiliert:

get @0 (Vec2f 0 1) 

und dies nicht:

get @4 (Vec2f 0 1) 

Nun frage ich mich, ob ich mit diesen Funktionen Laufzeitvergleiche schreiben kann. Ich versuchte dies:

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 

Ich glaube, ich habe Anwesenheit von Get i n e Instanz zur Laufzeit zu überprüfen, ist es eine Möglichkeit, es zu tun?

Answer 1

Ich glaube nicht, dass es einen einfachen Weg gibt.

Haskell ist so konzipiert, dass alle Arten von Zeug zur Laufzeit gelöscht werden können. Der einzige Weg, den ich davon kenne, ist, KnownNat und Typeable auszunutzen und manuell gegen jede Instanz zu überprüfen. Z.B. so etwas wie:

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 

(Dies könnte wahrscheinlich einige Factoring verwenden ...)

Wahrscheinlich ein besserer Ansatz wäre, eine Liste zu definieren (oder was auch immer) verdinglichter Wörterbücher und Schleife über sie. Man müsste diese Liste jedoch mit den tatsächlichen Instanzen synchronisieren.

Vielleicht wird Haskell in Zukunft auch die Klassensuchmaschine zur Laufzeit bekommen. Bisher wurde dies nicht getan, da der Wechsel zu Runtime-Typprüfungen in Haskell ziemlich unidiomatisch ist. Aber nachdem wir DataKinds und KnownNat und ähnliche Sachen bekommen haben, ist vielleicht die Verdinglichung/"Reflektion" von statischen Informationen zur Laufzeit interessanter geworden.

Answer 2

Ein Problem im Moment ist, dass Get Instanzen sind alle Arten von Ad-hoc, so dass es schwer ist, eine saubere Lösung bereitzustellen. Wenn Sie bereit sind Get ein wenig Refactoring, ist es viel einfacher:

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 ":(" 

Dann können Sie

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 von den typelits Zeugen Verwendung tun Bibliothek die Ungleichheitsbedingung in den Kontext zu bringen für GHC zu verwenden.