We extend the core semantics for Dependent Haskell with rules for ?·-equivalence. This semantics is defined by two related calculi, Systems D and DC. The first is a Curry-style dependently-typed language with nontermination, irrelevant arguments, and equality abstraction. The second, inspired by the Glasgow Haskell Compilera??s core language FC, is the explicitly-typed analogue of System D, suitable for implementation in GHC. Our work builds on and extends the existing metatheory for these systems developed using the Coq proof assistant.
展开▼
