2015-07-10 15 views
71

Das Papier "Programming and reasoning with algebraic effects and dependent types" by Edwin C. Brady auf Effekte in Idris enthält die (nicht referenzierte) behaupten, dass:"Monad Transformatoren leistungsfähiger als Effekte" - Beispiele?

Obwohl [Effekte und monadisch Transformatoren] in Kraft nicht gleichwertig sind - Monaden und monadisch Transformatoren können weitere Konzepte express - viele gemeinsame effekt Berechnungen gefangen.

Welche Beispiele gibt es, die von Monade-Transformatoren modelliert werden können, aber keine Effekte?

+21

Dies ist eine nützliche Frage, die von mehr Menschen beantwortet werden kann als nur der Autor des Papiers. Ein Beispiel für mehr Leistung sind doppelte Effekte. –

+5

Ich würde gerne die Antwort auf diese Frage wissen. Ich möchte nicht den Autor des Papiers kontaktieren müssen, wenn ich es hier nur finden könnte. – Xoltar

+3

Das ist eine gute Frage, auch wenn es etwas Papier erwähnt ... – Cynede

Antwort

8

Fortsetzungen können mit CPS als Monaden modelliert werden, aber sie sind keine algebraischen Effekte, da sie nicht mithilfe von Lawvere-Theorien modelliert werden können. Siehe Martin Hyland und John Power, 2007, The Category Theoretic Understanding of Universal Algebra: Lawvere Theories and Monads (pdf), ENTCS 172: 437-458.

+0

Danke für die Antwort. Ich denke darüber nach und versuche, die Kategorientheorie in etwas programmatischeres zu übersetzen, um meinen Kopf herumzukriegen. @Eduardo kommentierte oben, dass Effekte zu begrenzten Fortsetzungen isomorph waren. Ich vermute daher, dass es eine gewisse Intuition darüber gibt, dass unbegrenzte Fortsetzungen nicht modelliert werden können. Effekte müssen möglicherweise auf eine bestimmte Region beschränkt und gehandhabt werden, bevor wirksame Werte entkommen können, während Monaden ansteckender sind. –

+1

@geoff_h Ich sagte, dass algebraische Effekte als Verwendungen der abgegrenzten Fortsetzungs-Monade modelliert werden könnten, nicht dass sie äquivalent wären - was wohl der Fall sein könnte, aber ich weiß es nicht wirklich. – pyon

+0

@Eduardo Aber Eff erlaubt eine Darstellung von begrenzten Fortsetzungen - obwohl eine, die manchmal rekursive Typen erfordert. Dies legt einen Isomorphismus nahe - Effekte können als begrenzte Fortsetzungen modelliert werden, abgegrenzte Fortsetzungen können als Effekte modelliert werden - aber vielleicht kann Eff auch einige nicht-algebraische Effekte darstellen - obwohl ich mir nicht sicher bin, was ich a gut verstanden habe nicht-algebraische Wirkung würde bedeuten. –