Equality Proofs and Deferred Type Errors A Compiler Pearl

被引：16
|
作者：
Vytiniotis, Dimitrios [1 ]
Jones, Simon Peyton [1 ]
Magalhaes, Jose Pedro [2 ]
机构：
[1] Microsoft Res, Cambridge, England
[2] Univ Utrecht, NL-3508 TC Utrecht, Netherlands
来源：
ACM SIGPLAN NOTICES | 2012年 / 47卷 / 09期
基金：
英国工程与自然科学研究理事会;
关键词：
Design; Languages; Type equalities; Deferred type errors; System FC; LANGUAGE;
D O I：
10.1145/2398856.2364554
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
The Glasgow Haskell Compiler is an optimizing compiler that expresses and manipulates first-class equality proofs in its intermediate language. We describe a simple, elegant technique that exploits these equality proofs to support deferred type errors. The technique requires us to treat equality proofs as possibly-divergent terms; we show how to do so without losing either soundness or the zero-overhead cost model that the programmer expects.
引用
收藏
页码：341 / 352
页数：12
相关论文
共 50 条
  • [1] Equality of proofs for linear equality
    Dosen, Kosta
    Petric, Zoran
    [J]. ARCHIVE FOR MATHEMATICAL LOGIC, 2008, 47 (06) : 549 - 565
  • [2] Equality of proofs for linear equality
    Kosta Došen
    Zoran Petrić
    [J]. Archive for Mathematical Logic, 2008, 47 : 549 - 565
  • [3] Delta Debugging Type Errors with a Blackbox Compiler
    Sharrad, Joanna
    Chitil, Olaf
    Wang, Meng
    [J]. PROCEEDINGS OF THE 30TH SYMPOSIUM ON IMPLEMENTATION AND APPLICATION OF FUNCTIONAL LANGUAGES (IFL 2018), 2018, : 13 - 24
  • [4] The algebra of equality proofs
    Stump, A
    Tan, LY
    [J]. TERM REWRITING AND APPLICATIONS, PROCEEDINGS, 2005, 3467 : 469 - 483
  • [5] Generating Compiler Optimizations from Proofs
    Tate, Ross
    Stepp, Michael
    Lerner, Sorin
    [J]. ACM SIGPLAN NOTICES, 2010, 45 (01) : 389 - 402
  • [6] TOWARD COMPILER IMPLEMENTATION CORRECTNESS PROOFS
    CHIRICA, LM
    MARTIN, DF
    [J]. ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1986, 8 (02): : 185 - 214
  • [7] Generating Compiler Optimizations from Proofs
    Tate, Ross
    Stepp, Michael
    Lerner, Sorin
    [J]. POPL'10: PROCEEDINGS OF THE 37TH ANNUAL ACM SIGPLAN-SIGACT SYMPOSIUM ON PRINCIPLES OF PROGRAMMING LANGUAGES, 2010, : 389 - 402
  • [8] EQUALITY - AMERICAS DEFERRED COMMITMENT
    WOODWARD, CV
    [J]. AMERICAN SCHOLAR, 1958, 27 (04): : 459 - 472
  • [9] ERRORS IN MATHEMATICAL PROOFS
    ZAHLER, R
    [J]. SCIENCE, 1976, 193 (4248) : 98 - 98
  • [10] Proofs of numerical programs when the compiler optimizes
    Boldo, Sylvie
    Thi Minh Tuyen Nguyen
    [J]. INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING, 2011, 7 (02) : 151 - 160
12345