Hinzufügen einer Ord-Instanz zu 'Singleton'-Paket generierten Naturals

Question

Ich verwende sehr einfache Typ-Level-Naturals, die mit dem Singleton-Paket erzeugt wurden. Ich versuche nun, ihnen eine Ord-Instanz hinzuzufügen.

{-# LANGUAGE MultiParamTypeClasses, TemplateHaskell, KindSignatures, DataKinds, ScopedTypeVariables, GADTs, TypeFamilies, FlexibleInstances, TypeOperators, UndecidableInstances, InstanceSigs #-} 

module Functions where 

import Data.Singletons 
import Data.Singletons.TH 
import Data.Singletons.Prelude 
import Data.Promotion.Prelude 

singletons [d| 
      data Nat = Z | S Nat 
       deriving Eq 

      instance Ord Nat where 
       (<=) Z  _ = True 
       (<=) (S _) Z = False 
       (<=) (S n) (S m) = n <= m 
      |] 

Ich habe einen Fehler nach dem anderen getroffen. Der jüngste ist:

src/Functions.hs:10:1: 
    Couldn't match kind ‘Nat’ with ‘*’ 
    When matching types 
     n0 :: Nat 
     t1 :: * 
    Expected type: Sing t1 
     Actual type: Sing n0 
    Relevant bindings include 
     n_a9na :: Sing n0 (bound at src/Functions.hs:10:1) 
     lambda :: Sing n0 -> Sing m0 -> Sing (Apply (Apply (:<=$) t00) t10) 
     (bound at src/Functions.hs:10:1) 
    In the second argument of ‘applySing’, namely ‘n_a9na’ 
    In the first argument of ‘applySing’, namely 
     ‘applySing (singFun2 (Proxy :: Proxy (:<=$)) (%:<=)) n_a9na’ 

src/Functions.hs:10:1: 
    Could not deduce (SOrd 'KProxy) arising from a use of ‘%:<=’ 
    from the context (t00 ~ 'S n) 
     bound by a pattern with constructor 
       SS :: forall (z_a9mg :: Nat) (n_a9mh :: Nat). 
         (z_a9mg ~ 'S n_a9mh) => 
         Sing n_a9mh -> Sing z_a9mg, 
       in an equation for ‘%:<=’ 
     at src/Functions.hs:(10,1)-(18,15) 
    or from (t10 ~ 'S n1) 
     bound by a pattern with constructor 
       SS :: forall (z_a9mg :: Nat) (n_a9mh :: Nat). 
         (z_a9mg ~ 'S n_a9mh) => 
         Sing n_a9mh -> Sing z_a9mg, 
       in an equation for ‘%:<=’ 
     at src/Functions.hs:(10,1)-(18,15) 
    or from (t00 ~ Apply SSym0 n0, t10 ~ Apply SSym0 m0) 
     bound by the type signature for 
       lambda_a9n9 :: (t00 ~ Apply SSym0 n0, t10 ~ Apply SSym0 m0) => 
           Sing n0 -> Sing m0 -> Sing (Apply (Apply (:<=$) t00) t10) 
     at src/Functions.hs:(10,1)-(18,15) 
    In the second argument of ‘singFun2’, namely ‘(%:<=)’ 
    In the first argument of ‘applySing’, namely 
     ‘singFun2 (Proxy :: Proxy (:<=$)) (%:<=)’ 
    In the first argument of ‘applySing’, namely 
     ‘applySing (singFun2 (Proxy :: Proxy (:<=$)) (%:<=)) n_a9na’ 

Hat jemand eine Idee, was der richtige Weg, dies zu tun ist?

Answer 1

Ich bin mir nicht sicher, warum das scheitert. Ich bin ebenso durch ein ähnliches Versagen verwirrt ich erhalte, wenn compare statt Implementierung und noch mehr verwirrt durch das Scheitern ich bekomme, wenn die (scheinbar einfache) versucht

singletons [d| data Nat = Z | S Nat deriving (Eq,Ord) |] 

Meine Vermutung ist, dass etwas in Ord weg ist ... Das funktioniert jedoch. Ich werde versuchen, später einen Blick auf den Mut von singleton zu werfen.

singletons [d| 
       data Nat = Z | S Nat 
       deriving (Eq) 

       instance Ord Nat where 
       compare = compare' 

       compare' :: Nat -> Nat -> Ordering 
       compare' Z Z = EQ 
       compare' (S _) Z = GT 
       compare' Z (S _) = LT 
       compare' (S n) (S m) = compare' n m 
      |] 

Übrigens verwende ich GHC 8.0 hier.

EDIT

Nach etwa in singletons Stossen, habe ich die wahre Quelle der Probleme gefunden (und hackery ist möglich, mit wie viel Typ-Ebene weggeblasen worden ist). Unter Verwendung -ddump-splices von GHC konnte ich den tatsächlichen erzeugten Haskell Code erhalten (für den Anfangscode in Ihrer Frage). Die beanstandeten Teile waren

instance PEq (Proxy :: Proxy Nat_a7Vb) where 
    type (:==) (a_a8Rs :: Nat_a7Vb) (b_a8Rt :: Nat_a7Vb) = Equals_1627424016_a8Rr a_a8Rs b_a8Rt 

und

instance POrd (Proxy :: Proxy Nat_a7Vb) where 
    type (:<=) (a_aa9e :: Nat_a7Vb) (a_aa9f :: Nat_a7Vb) = Apply (Apply TFHelper_1627428966Sym0 a_aa9e) a_aa9f 

Kompilieren des Codes erzeugt, I die etwas nützlichere Fehlermeldung für beide

empfangenen

Expecting one more argument to ‘Proxy’ 
Expected kind ‘Proxy Nat_a7Vb’, but ‘Proxy’ has kind ‘k0 -> *’ 

im Zusammenhang mit der (Proxy :: Proxy Nat_a7Vb) im PEq und POrd Klassen. Das kompiliert nicht ohne -XPolyKinds. Checked das Repo für singletons und in der Tat es sagt Ihnen, dass Sie -XTypeInType aktiviert, die wiederum ermöglicht -XPolyKinds.

So gibt es keine Fehler, Sie müssen nur hinzufügen, entweder PolyKinds oder TypeInType (I letzteres empfehlen, denn das ist, was das Paket empfiehlt ...), um Ihre LANGUAGE pragmas alles zu bekommen zu arbeiten.

Answer 2

Mit angehobenen booleschen Beziehungen arbeiten isnevercomfortable. Booleans löschen genau die Informationen aus, an denen Sie interessiert sind, und lassen Sie im Stich, wenn Sie etwas mit dem Ergebnis Ihres Tests machen wollen. Sag einfach nein, Kinder.

Es gibt einen besseren Weg. „n ist weniger als oder gleich m“ ist ein Satz diebewiesen mit informationsreichen Beweis sein kann.Eine Möglichkeit, zu beweisen, dass eine Zahl kleiner als die andere ist, indem (eine Singleton-Darstellung) ihre Differenz:

data LE n m where 
    LE :: Natty z -> LE n (n :+ z) 

Wir können mit einem Verfahren kommen zur Prüfung, ob eine bestimmte Zahl kleiner als eine andere. le versucht, n von m zu subtrahieren, und entweder schlägt fehl und gibt Nothing zurück oder erzeugt ihre Differenz als Natty, und ein Beweis, dass die Subtraktion korrekt ist, verpackt in der LE Konstruktor.

le :: Natty n -> Natty m -> Maybe (LE n m) 
le Zy m = Just (LE m) 
le (Sy n) (Sy m) = fmap (\(LE z) -> LE z) (le n m) 
le _ _ = Nothing 

Diese Idee kann uns verallgemeinert werden, um eine „compare stark typisierte“ zu geben. Wenn Sie zwei Zahlen vergleichen, werden Sie entweder lernen, dass sie gleich sind oder dass eine weniger ist als die andere. (Either (LE n m) (LE m n) tut auch den Job, aber diese Version ist etwas präziser.)

data Compare n m where 
    LT :: Natty z -> Compare n (n :+ S z) 
    EQ :: Compare n n 
    GT :: Natty z -> Compare (m :+ S z) m 

compare :: Natty n -> Natty m -> Compare n m 
compare Zy Zy = EQ 
compare Zy (Sy m) = LT m 
compare (Sy n) Zy = GT n 
compare (Sy n) (Sy m) = case compare n m of 
    LT z -> LT z 
    EQ -> EQ 
    GT z -> GT z 

(ich dies aus Hasochism angehoben.)

Beachten Sie, dass im Gegensatz zu le, compare insgesamt ist. Es wird immer geben Sie ein Ergebnis: jede Zahl ist entweder kleiner als, gleich oder größer als jede andere Zahl. Unser Ziel war es, eine Prozedur zu schreiben, um zu testen, welche von zwei Zahlen kleiner war, aber wir fanden auch heraus, dass Zahlen totally ordered sind, und schreiben eine typsichere Subtraktionsroutine, alle in derselben Funktion.

Eine andere Sichtweise auf compare ist als Ansicht über Paare von natürlichen Zahlen. Wenn Sie zwei Zahlen miteinander vergleichen, erfahren Sie, um welche Zahl es sich bei welchen Zahlen handelt und um wie viel. Agda der Punkt-Muster haben eine gute Unterstützung für diese Idee der Verfeinerung:

compare : (n m : Nat) -> Compare n m 
compare zero zero = eq 
compare zero (suc m) = lt m 
compare (suc n) zero = gt n 
compare (suc n)   (suc m)   with compare n m 
         -- see how matching on `lt` refines `m` to `n + suc z` 
compare (suc n)   (suc .(n + suc z)) | lt z = lt z 
compare (suc m)   (suc .m)   | eq = eq 
    -- likewise matching on `gt` refines `n` to `m + suc z` 
compare (suc .(m + suc z)) (suc m)   | gt z = gt z 

---

Wie dem auch sei, ich kann nicht direkt an die Quelle Ihrer singletons Fehler sprechen, aber ein Grund Ord ist ein bisschen schwierig zu verarbeiten, für Singleton Werte ist, dass es Sie vergleichen Werte des gleichen Typs gelten folgende Voraussetzungen:

class Ord a where 
    compare :: a -> a -> Ordering 

Wenn Sie zwei Singletons sind zu vergleichen, werden sie in der Regel nicht die gleiche Art haben! Das ist der springende Punkt von Singletons: Ihr Typ spiegelt ihren Wert direkt wider. Wenn Sie zwei Natty n Werte haben (deren n s übereinstimmen), ist es nicht viel Sinn, sie zu vergleichen, da Sie bereits wissen, dass sie gleich sind; und wenn sie nicht gleich sind, kannst du sie nicht vergleichen!

Es ist eminent vernünftig, dass Klassen wie Ord, die in der einfach typisierten Welt entwickelt wurden, nicht unbedingt nützlich in abhängige Programme sein werden. Wenn Sie abhängige Typen verwenden, sollten Sie die alten Tools nicht missbrauchen. Usher in dieser neuen Welt der sicheren, informationsreichen Programmierung mit offenen Armen!