Effect Polymorphism in Higher-Order Logic (Proof Pearl)

被引：0
|
作者：
Andreas Lochbihler
机构：
[1] Digital Asset (Switzerland) GmbH,
来源：
Journal of Automated Reasoning | 2019年 / 63卷
关键词：
Monad; Monad transformer; Effects; Polymorphism; Equational reasoning; Isabelle/HOL;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
The notion of a monad cannot be expressed within higher-order logic (HOL) due to type system restrictions. I show that if a monad is restricted to values of a fixed type, this notion can be formalised in HOL. Based on this idea, I develop a library of effect specifications and implementations of monads and monad transformers. Hence, I can abstract over the concrete monad in HOL definitions and thus use the same definition for different (combinations of) effects. I illustrate the usefulness of effect polymorphism with a monadic interpreter.
引用
下载
收藏
页码：439 / 462
页数：23
相关论文
共 50 条
  • [31] Extensional Higher-Order Logic Programming
    Charalambidis, Angelos
    Handjopoulos, Konstantinos
    Rondogiannis, Panagiotis
    Wadge, William W.
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2013, 14 (03)
  • [32] HIGHER-ORDER ILLATIVE COMBINATORY LOGIC
    Czajka, Lukasz
    JOURNAL OF SYMBOLIC LOGIC, 2013, 78 (03) : 837 - 872
  • [33] Learning higher-order logic programs
    Cropper, Andrew
    Morel, Rolf
    Muggleton, Stephen
    MACHINE LEARNING, 2020, 109 (07) : 1289 - 1322
  • [34] Modal Pluralism and Higher-Order Logic
    Clarke-Doane, Justin
    McCarthy, William
    PHILOSOPHICAL PERSPECTIVES, 2022, 36 (01) : 31 - 58
  • [35] Learning higher-order logic programs
    Andrew Cropper
    Rolf Morel
    Stephen Muggleton
    Machine Learning, 2020, 109 : 1289 - 1322
  • [36] RESULTS IN HIGHER-ORDER MODAL LOGIC
    GALLIN, D
    JOURNAL OF SYMBOLIC LOGIC, 1974, 39 (01) : 197 - 198
  • [37] SOME REMARKS ON HIGHER-ORDER LOGIC
    KOGALOVSKII, SR
    DOKLADY AKADEMII NAUK SSSR, 1968, 178 (05): : 1007 - +
  • [38] REMARKS ON HIGHER-ORDER MODAL LOGIC
    DACOSTA, NCA
    DEALCANTARA, LP
    ACTA CIENTIFICA VENEZOLANA, 1987, 38 (02): : 282 - 284
  • [39] Refinement of higher-order logic programs
    Colvin, R
    Hayes, I
    Hemer, D
    Strooper, P
    LOGIC BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2003, 2664 : 126 - 143
  • [40] HIGHER-ORDER LOGIC LEARNING AND λPROGOL
    Pahlavi, Niels
    TECHNICAL COMMUNICATIONS OF THE 26TH INTERNATIONAL CONFERENCE ON LOGIC PROGRAMMING (ICLP'10), 2010, 7 : 281 - 285
12345