konnte SingI des Vorgängers nicht ableiten Nat

Question

Ich versuche, eine weaken Funktion für endliche Mengen von ganzen Zahlen zu schreiben. Ich verwende das singletons Paket. Ich habe Additions-, Subtraktions- und Vorgängerfunktionen definiert und gefördert sowie einige Gleichungen auf ihnen getestet, um dem Typ-Checker zu helfen. Aber der Fehler, den ich bekommen habe, steht damit nicht in Zusammenhang.

weaken :: forall n m k . (SingI n, SingI m, SingI k, (Minus m n) ~ NatJust k) => Fin n -> Fin m 
weaken ZF = gcastWith (apply Refl $ plus_minus sm sn sk) ZF 
    where sn = sing :: SNat n 
     sm = sing :: SNat m 
     sk = sing :: SNat k 
weaken (SF n) = gcastWith (apply Refl $ succ_pred sm) (SF (weaken n)) 
    where sn = sing :: SNat n 
     sm = sing :: SNat m 
     sk = sing :: SNat k 

Der Fehler Ich erhalte auf der rekursiven Aufruf von weaken (SF (weaken n)) und ist die folgende: Could not deduce (SingI n1), wo n1 richtig gefolgert wird der Typ-Ebene Vorgänger vom Typ n zu sein. I könnte fügen Sie eine SingI (Pred n) Einschränkung, aber dies bewegt einfach das Problem eine Ebene nach unten (GHC sagt jetzt, es kann nicht das Äquivalent von (SingI (Pred (Pred n))) abzuleiten).

Wie kann ich GHC davon überzeugen, dass SingI (Pred n) aus SingI n folgt (und warum das singletons Paket dies bereits tut)?

Answer 1

GHC.TypeLits, die uns schließlich Typ-Level-nicht-negative Integer -s liefert, exportiert keine Funktionen, die uns Singleton Runtime-Operationen machen würde. Zum Beispiel gibt es KnownNat a und KnownNat b, es gibt keine Standardfunktion, KnownNat (a + b) zur Laufzeit zu produzieren.

singletons löst dies durch die Implementierung der singleton Nat operations unsicher.

singletons Subtraktion Funktion löst einen Fehler für negative Ergebnisse (und gestutzt nicht auf 0, wie wir wollen würde), so können wir nicht, dass die Wiederverwendung für pred und haben es implementieren uns:

{-# language TypeApplications #-} -- plus all the usual exts 

import Data.Singletons.Prelude 
import Data.Singletons.TypeLits 
import Unsafe.Coerce 

type family Pred (n :: Nat) :: Nat where 
    Pred 0 = 0 
    Pred n = n :- 1 

sPred :: Sing n -> Sing (Pred n) 
sPred sn = case fromSing sn of 
    0 -> unsafeCoerce (sing @_ @0) 
    n -> case toSing @Nat (n - 1) of 
    SomeSing sn -> unsafeCoerce sn 

Sie können sPred verwenden, um Sing (Pred n), dann withSingI oder singInstance zu erhalten, um das in SingI (Pred n) umzuwandeln.

Sie sollten jedoch wahrscheinlich SingI in weaken nicht verwenden. Der Zweck von SingI ist, Singleton-Parameter automatisch in Kontexten zu verbinden, in denen Sie sie für nichts anderes als Weiterleitung an andere Funktionen verwenden. Verwenden Sie stattdessen einfach Sing, und vermeiden Sie sing und geben Sie Annotationsrauschen ein. Meiner Erfahrung nach ist Sing in etwa 90% der Zeit SingI für singletons Programmierung vorzuziehen.