Here ist ein funktionales Programmierrätsel, bei dem es um das Verknüpfen von Schleifen und unendliche Datenstrukturen geht. Es gibt ein bisschen Hintergrund, also bleibt dran.

Die Einstellung Definieren wir einen Datentyp, der rekursive Datentypen darstellt:

type Var = String
data STerm = SMu Var STerm
           | SVar Var
           | SArrow STerm STerm
           | SBottom
           | STop
   deriving (Show)

d.h.t ::= μα. t | α | t → t | ⊥ | ⊤. Man beachte, dass ⊥ den Typ ohne Einwohner bezeichnet, während ⊤ den Typ mit allen Einwohnern bezeichnet. Beachten Sie, dass(μα. α) = ⊥, da μ ein @ iam wenigste fixpoint operator.

Wir können einen rekursiven Datentyp als unendlichen Baum interpretieren, der durch wiederholtes Entfalten entstehtμα. t zut[α ↦ μα. t]. (Eine formale Beschreibung dieses Vorgangs finden Sie unterhttp: //lucacardelli.name/Papers/SRT.pd) In Haskell können wir einen Typ von Lazy Trees definieren, die keine μ-Binder oder Variablen haben:

data LTerm = LArrow LTerm LTerm
           | LBottom
           | LTop
   deriving (Show)

und, in gewöhnlichen Haskell, eine Konvertierungsfunktion von einem zum anderen:

convL :: [(Var, LTerm)] -> STerm -> LTerm
convL _ STop    = LTop
convL _ SBottom = LBottom
convL ctx (SArrow t1 t2) = LArrow (convL ctx t1) (convL ctx t2)
convL ctx (SVar v)
    | Just l <- lookup v ctx = l
    | otherwise = error "unbound variable"
convL ctx (SMu v t) = fix (\r -> convL ((v, r) : ctx) t)

Es gibt jedoch ein Problem mit dieser Funktion: Sie ist nicht produktiv. Wenn du läufstconvL [] (SMu "x" (SVar "x")) Sie werden Endlosschleife. Wir würden lieber @ bekommLBottom in diesem Fall. Eine interessante Übung besteht darin, diese Funktion direkt so zu korrigieren, dass sie produktiv ist. in dieser frage möchte ich das problem jedoch anders lösen.

Produktivität mit der Verzögerungsmodalität. Wenn wir zyklische Datenstrukturen wie oben erstellen, müssen wir sicherstellen, dass wir die Ergebnisse unserer Berechnungen nicht verwenden, bevor wir sie erstellt haben. Die Verzögerungsmodalität ist ein Weg, um sicherzustellen, dass wir produktive (nicht endlose Schleifen) Programme schreiben. Die Grundidee ist einfach: Wenn der TypInt bedeutet, dass ich heute eine ganze Zahl habe, ich definiere einen TypkonstruktorD, damitD Int bedeutet, dass ich einen Wert vom Typ @ haInt Morge. D ist ein Functor und ein Applicative (aber KEINE Monade.)

-- D is abstract; you are not allowed to pattern match on it
newtype D a = D a
   deriving (Show)

instance Functor D where
    fmap f (D a) = D (f a)

instance Applicative D where
    D f <*> D a = D (f a)
    pure x = D x

MitD definieren wir einen Fixpunktoperator: er besagt, dass ein Wert von @ konstruiert werden soa, Sie können auf das @ zugreifa du konstruierst, solange du es nur benutztMorge.

fixD :: (D a -> a) -> a
fixD f = f (D (fixD f))

Beispielsweise besteht ein Stream aus einem Werta Ich habe heute und einen StreamStream a was ich morgen produzieren muss.

data Stream a = Cons a (D (Stream a))

UsingfixD, Ich kann ein @ definiermap Funktion auf Streams, die @ igarantier um produktiv zu sein, da der rekursive Aufruf vonmap wird nur verwendet, um Werte zu erzeugen, die morgen benötigt werden.

instance Functor Stream where
    fmap f = fixD $ \go (Cons x xs) -> Cons (f x) (go <*> xs)

Das Problem Hier ist eine Variante vonLTerm mit einer expliziten Verzögerungsmodalität.

data Term = Arrow (D Term) (D Term)
          | Bottom
          | Top
    deriving (Show)

UsingfixD (keine nicht-strukturell rekursiven Referenzen erlaubt), wie schreibe ich eine Funktionconv :: STerm -> Term (oderconv :: STerm -> D Term)? Ein besonders interessanter Testfall istSMu "x" (SArrow STop (SMu "y" (SVar "x"))); es sollte keine Bottoms in der resultierenden Struktur geben!

Aktualisieren Ich habe versehentlich eine strukturelle Rekursion auf @ ausgeschlossSTerm, was nicht die Absicht der Frage war; Ich habe umformuliert, um diese Einschränkung zu entfernen.