Einschränken von Datentypen

Question

Angenommen, Sie haben eine schöne induktive Definition, die Sie in Haskell als Datentyp definieren möchten. Ihre induktive Definition ist jedoch (so viele induktive Definitionen) von einer solchen Form, dass die Erzeugungsregeln ihre "Prämissen" benötigen, um eine bestimmte Struktur zu haben. Zum Beispiel: Angenommen wir die folgende Definition haben:

• wenn x eine gerade ganze Zahl, dann ist T x eine Waffe,
• wenn x eine ungerade ganze Zahl ist, dann S x eine Waffe ist.

Wenn ich das definieren will (als Einzel) Datentyp in Haskell, würde ich so etwas wie

data Weapon = T Int | S Int 

Offensichtlich schreiben, das wird nicht funktionieren, wie Sie jetzt T 5 und S 4 erzeugen können, für Beispiel. Gibt es eine natürliche Möglichkeit, Einschränkungen für die Konstruktorargumente weiterzuleiten, so dass ich etwas Ähnliches wie den obigen Code schreiben könnte, der die richtige Definition geben würde?

Answer 1

Ihr bester Schuss ist nicht T und S explizit zu exportieren, aber einem benutzerdefinierten Konstruktor erlauben:

module YourModule (Weapon, smartConstruct) where 

data Weapon = T Int | S Int 

smartConstruct :: Int -> Weapon 
smartConstruct x 
    | even x  = T x 
    | otherwise = S x 

Nun, wenn YourModule Import Benutzer nicht in der Lage zu erstellen T und S explizit, sondern nur mit Ihre smartConstruct Funktion.

Answer 2

Dies ist ein bisschen un-Haskelly, aber ist idiomatischer in z.B. Agda: Ändere die Interpretation deiner Darstellung, so dass sie durch die Konstruktion korrigiert werden muss.

In diesem Fall beachten Sie, dass wenn n :: Int, dann even (2 * n) und odd (2 * n + 1). Wenn wir den Fall von zu großen Int s Handwave wegwinken, können wir sagen, dass es eine Bijektion zwischen den geraden Int s und Int s gibt; und ein weiterer zwischen den ungeraden Int s und der Int s.

diese So verwenden, können Sie diese Darstellung wählen:

data Weapon = T Int | S Int 

und seine Auslegung so ändern, dass der Wert T n repräsentiert tatsächlich T (2 * n) und S n der Wert repräsentiert S (2 * n + 1). Egal, was n :: Int Sie wählen, T n wird gültig sein, da Sie es als den "T -of-2 * n" Wert betrachten werden.

Answer 3

Wenn Sie bereit sind, sich auf die Verwendung von Nats zu beschränken, und mit der Verwendung einigermaßen fortgeschrittener Typenmagie einverstanden sind, können Sie GHC.TypeLits verwenden.

{-# LANGUAGE DataKinds, GADTs, TypeOperators, KindSignatures #-} 

import GHC.TypeLits 

data Weapon (n :: Nat) where 
    Banana  :: n ~ (2 * m) => Weapon n 
    PointyStick :: n ~ (2 * m + 1) => Weapon n 

banana :: Weapon 2 
banana = Banana 

pointyStick :: Weapon 3 
pointyStick = PointyStick 

versuchen Sie für sich selbst, dass es nicht mit falschen (ungeraden/geraden) Zahlen kompilieren wird.

Edit: Praktischer ist wahrscheinlich Kaktus 'Ansatz obwohl.