Erfahrungsberichte mit indizierten Monaden in der Produktion?

Question

In einer früheren Frage entdeckte ich die Existenz von Conor McBride Kleisli arrows of Outrageous Fortune bei der Suche nach Möglichkeiten der Codierung Idris examples in Haskell. Meine Bemühungen McBride Code zu verstehen und sie in Haskell machen kompilieren zu diesem Kern geführt: https://gist.github.com/abailly/02dcc04b23d4c607f33dca20021bcd2f

Während auf Hackage suchen, habe ich mehrere Implementierungen dieser Konzepte entdeckt, vor allem durch (erraten, wer?) Edward Kmett und Gabriel Gonzalez.

Welche Erfahrungen haben Menschen mit der Erstellung eines solchen Codes? Insbesondere, treten die erwarteten Vorteile (Laufzeitsicherheit, selbststeuernde Nutzung) tatsächlich IRL auf? Wie wäre es mit dieser Art von Code im Laufe der Zeit und Onboarding Newcomer?

BEARBEITEN: Ich änderte den Titel, um genauer zu sein über das, was ich suche: Real-World-Verwendung von indizierten Monaden in freier Wildbahn. Ich bin daran interessiert, sie zu verwenden, und ich habe mehrere Anwendungsfälle im Hinterkopf, nur frage mich, ob andere Leute sie bereits in "Produktion" Code verwendet haben.

EDIT 2: Dank der großartigen Antworten, die bisher zur Verfügung gestellt wurden, und nützlichen Kommentaren habe ich den Titel und die Beschreibung dieser Frage erneut bearbeitet, um genauer zu reflektieren, welche Art von Antwort ich erwarte, z. Erfahrungsbericht.

Answer 1

Ich denke, die folgenden sollten als ein praktisches Beispiel zählen: Statisch "Well-Stackedness" in einem Compiler durchsetzen. Vorformulierten zuerst:

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

import qualified Prelude 
import Prelude hiding (return, fail, (>>=), (>>)) 

Dann eine einfache Stapel Sprache:

data Op (i :: [*]) (j :: [*]) where 
    IMM :: a -> Op i (a ': i) 
    BINOP :: (a -> b -> c) -> Op (a ': b ': i) (c ': i) 
    BRANCH :: Label i j -> Label i j -> Op (Bool ': i) j 

und wir werden nicht mit echten Label s stören:

data Label (i :: [*]) (j :: [*]) where 
    Label :: Prog i j -> Label i j 

und Prog Widder sind nur typausgerichtet Listen von Op s:

data Prog (i :: [*]) (j :: [*]) where 
    PNil :: Prog i i 
    PCons :: Op i j -> Prog j k -> Prog i k 

So können wir in dieser Einstellung sehr leicht einen Compiler machen, der eine indizierte Schreiber-Monade ist; das heißt, eine indizierte Monade:

class IMonad (m :: idx -> idx -> * -> *) where 
    ireturn :: a -> m i i a 
    ibind :: m i j a -> (a -> m j k b) -> m i k b 

-- For RebindableSyntax, so that we get that sweet 'do' sugar 
return :: (IMonad m) => a -> m i i a 
return = ireturn 
(>>=) :: (IMonad m) => m i j a -> (a -> m j k b) -> m i k b 
(>>=) = ibind 
m >> n = m >>= const n 
fail = error 

, die eine (n indizierte) Monoid ermöglicht Akkumulieren:

class IMonoid (m :: idx -> idx -> *) where 
    imempty :: m i i 
    imappend :: m i j -> m j k -> m i k 

wie normale Writer:

newtype IWriter w (i :: [*]) (j :: [*]) (a :: *) = IWriter{ runIWriter :: (w i j, a) } 

instance (IMonoid w) => IMonad (IWriter w) where 
    ireturn x = IWriter (imempty, x) 
    ibind m f = IWriter $ case runIWriter m of 
     (w, x) -> case runIWriter (f x) of 
      (w', y) -> (w `imappend` w', y) 

itell :: w i j -> IWriter w i j() 
itell w = IWriter (w,()) 

So einfach wenden wir diese Maschinen Prog Rams:

instance IMonoid Prog where 
    imempty = PNil 
    imappend PNil prog' = prog' 
    imappend (PCons op prog) prog' = PCons op $ imappend prog prog' 

type Compiler = IWriter Prog 

tellOp :: Op i j -> Compiler i j() 
tellOp op = itell $ PCons op PNil 

label :: Compiler i j() -> Compiler k k (Label i j) 
label m = case runIWriter m of 
    (prog,()) -> ireturn (Label prog) 

und dann können wir versuchen, eine einfache Ausdruck Sprache kompilieren:

data Expr a where 
    Lit :: a -> Expr a 
    And :: Expr Bool -> Expr Bool -> Expr Bool 
    Plus :: Expr Int -> Expr Int -> Expr Int 
    If :: Expr Bool -> Expr a -> Expr a -> Expr a 

compile :: Expr a -> Compiler i (a ': i)() 
compile (Lit x) = tellOp $ IMM x 
compile (And x y) = do 
    compile x 
    compile y 
    tellOp $ BINOP (&&) 
compile (Plus x y) = do 
    compile x 
    compile y 
    tellOp $ BINOP (+) 
compile (If b t e) = do 
    labThen <- label $ compile t 
    labElse <- label $ compile e 
    compile b 
    tellOp $ BRANCH labThen labElse 

und wenn wir zum Beispiel weggelassen

compile (And x y) = do 
    compile x 
    tellOp $ BINOP (&&) 

• konnte nicht ableiten: i ~ (Bool : i) aus dem Kontext: eines der Argumente zu BINOP, wird die typechecker dies erkennen a ~ Bool

Answer 2

Ein weiteres schönes Beispiel ist mutexes mit Schloss Unlock-Check zur Kompilierzeit. Sie können dieses Beispiel auf Stephen Diehl Website:

http://dev.stephendiehl.com/hask/#indexed-monads

Answer 3

Session-Typen sind ein Versuch, Typ-Level-Beschreibungen zu Netzwerkprotokollen zu geben. Die Idee ist, dass, wenn ein Client einen Wert sendet, der Server bereit sein muss, diesen zu empfangen, und umgekehrt.

Also hier ist ein Typ (mit TypeInType) beschreibt Sitzungen bestehen aus einer Sequenz von Werten zu senden und Werte zu erhalten.

infixr 5 :!, :? 
data Session = Type :! Session 
      | Type :? Session 
      | E 

a :! s bedeutet "a einen Wert vom Typ senden, dann mit dem Protokoll weiter s". a :? s bedeutet "empfange einen Wert vom Typ a, dann fahre mit dem Protokoll s fort".

So Session stellt eine (Typ-Ebene) Liste von Aktionen. Unsere monadischen Berechnungen werden sich entlang dieser Liste bewegen und Daten senden und empfangen, wie es der Typ erfordert. Genauer gesagt reduziert eine Berechnung des Typs Chan s t a die verbleibende Arbeit, die zur Erfüllung des Protokolls von s bis t zu leisten ist. Ich werde Chan mit der indexierten freien Monade bauen, die ich in meiner Antwort auf Ihre andere Frage verwendet habe.

class IFunctor f where 
    imap :: (a -> b) -> f i j a -> f i j b 
class IFunctor m => IMonad m where 
    ireturn :: a -> m i i a 
    (>>>=) :: m i j a -> (a -> m j k b) -> m i k b 


data IFree f i j a where 
    IReturn :: a -> IFree f i i a 
    IFree :: f i j (IFree f j k a) -> IFree f i k a 

instance IFunctor f => IFunctor (IFree f) where 
    imap f (IReturn x) = IReturn (f x) 
    imap f (IFree fx) = IFree (imap (imap f) fx) 

instance IFunctor f => IMonad (IFree f) where 
    ireturn = IReturn 
    IReturn x >>>= f = f x 
    IFree fx >>>= f = IFree (imap (>>>= f) fx) 

Unsere Basis Aktionen im Chan Monade einfach Werte senden und empfangen.

data ChanF s t r where 
    Send :: a -> r -> ChanF (a :! s) s r 
    Recv :: (a -> r) -> ChanF (a :? s) s r 

instance IFunctor ChanF where 
    imap f (Send x r) = Send x (f r) 
    imap f (Recv r) = Recv (fmap f r) 

send :: a -> Chan (a :! s) s() 
send x = IFree (Send x (IReturn())) 

recv :: Chan (a :? s) s a 
recv = IFree (Recv IReturn) 

type Chan = IFree ChanF 
type Chan' s = Chan s E -- a "complete" Chan 

send nimmt den aktuellen Status der Sitzung a :! s-s, die Erfüllung der Verpflichtung ein a zu senden. Analog transformiert recv eine Sitzung von a :? s zu s.

Hier ist der lustige Teil. Wenn ein Ende des Protokolls einen Wert sendet, muss das andere Ende bereit sein, es zu empfangen, und umgekehrt. Dies führt zu der Idee einer Dual Sitzung Typ:

type family Dual s where 
    Dual (a :! s) = a :? Dual s 
    Dual (a :? s) = a :! Dual s 
    Dual E = E 

In insgesamt Sprache Dual (Dual s) = s beweisbar wäre, aber leider Haskell ist nicht insgesamt.

Sie können ein Paar von Kanälen verbinden, wenn ihre Typen dual sind. (Ich denke, man dies eine im Speicher nennen würde Simulation einen Client und einen Server zu verbinden.)

connect :: Chan' s a -> Chan' (Dual s) b -> (a, b) 
connect (IReturn x) (IReturn y) = (x, y) 
connect (IReturn _) (IFree y) = case y of {} 
connect (IFree (Send x r)) (IFree (Recv f)) = connect r (f x) 
connect (IFree (Recv f)) (IFree (Send y r)) = connect (f y) r 

Zum Beispiel, hier ist ein Protokoll für einen Server, der prüft, ob eine Zahl größer als 3 ist.Der Server wartet auf den Empfang einer Int, sendet eine Bool zurück und beendet dann die Berechnung.

type MyProtocol = Int :? Bool :! E 

server :: Chan' MyProtocol() 
server = do -- using RebindableSyntax 
    x <- recv 
    send (x > 3) 

client :: Chan' (Dual MyProtocol) Bool 
client = do 
    send 5 
    recv 

Und um es zu testen:

ghci> connect server client 
((),True) 

Session-Typen sind ein Gebiet der aktiven Forschung. Diese spezielle Implementierung ist für sehr einfache Protokolle geeignet, aber Sie können keine Protokolle beschreiben, bei denen der Typ der Daten, die über die Leitung gesendet werden, vom Zustand des Protokolls abhängt. Dafür braucht man Überraschungsüberraschung, abhängige Typen. Eine kurze Demonstration des Stands der Technik von Sitzungstypen finden Sie unter this talk by Brady.