<p>I do not know how much of the paper it covers but we do have a module based on it in the standard library:</p>

<p><a href="https://agda.github.io/agda-stdlib/Data.Record.html" rel="nofollow noreferrer">https://agda.github.io/agda-stdlib/Data.Record.html</a></p>

CC BY-SA 4.0
2019-09-03T12:02:33.387Z
This is extremely close to what I want/need. I was hoping to internalize disjointness conditions, rather than use shadowing (as Pollack, and thus the code, does). Thus my interest in Data.List.Fresh.
Jacques Carette
CC BY-SA 4.0
2019-09-03T12:48:43.820Z
By the way Fresh is nothing new, a version of it appears in Catarina Coquand's https://link.springer.com/article/10.1023/A:1019964114625
(I'll update the PR to give credits)
gallais
CC BY-SA 4.0
2019-09-03T12:52:38.967Z
For my use cases, not-new is better; too many innovations at once is suspicious. But thanks for the reference.
Jacques Carette
CC BY-SA 4.0
2019-09-03T10:03:46.657Z
2019-09-03T10:03:46.657Z
gallais
<p>Has anyone formalized Pollack's <a href="https://link.springer.com/article/10.1007/s001650200018" rel="nofollow noreferrer">Dependently Typed Records in Type Theory</a> ? Agda would be preferred, but anyone close to MLTT would work.  Weaker versions would be fine too, i.e. what Luo dubs 'dependently kinded records would be appreciated as well.</p>

<p>Full reference:</p>

<pre><code>@Article{Pollack2002,
author="Pollack, Robert",
title="Dependently Typed Records in Type Theory",
journal="Formal Aspects of Computing",
year="2002",
month="Jul",
day="01",
volume="13",
number="3",
pages="386--402",
abstract="The language Pebble of Burstall and Lampson proposed dependent types as the underlying principle in a unified framework to explain facilities for programming in the large, such as modules and signatures, as well as for programming in the small. This proposal soon extended to large scale formal proof development as well. In fact, the functional approach to modularity has turned out to be a hard problem, which is still far from a fully satisfactory solution. This paper discusses aspects of this approach, including representations of records, informative signatures, sharing, and subtyping. My main contribution in this paper is to show that structures with dependent types and manifest fields (roughly ML style modules) are internally definable in a type theoretic framework extended with inductive-recursive definition. This shows that powerful modules follow from general principles without module-specific assumptions.",
issn="1433-299X",
doi="10.1007/s001650200018",
url="https://doi.org/10.1007/s001650200018"
}
</code></pre>

<dependent-type><agda>
Formalization of dependent record types/kinds in MLTT or variant thereof?
Jacques Carette
# Formalization of dependent record types/kinds in MLTT or variant thereof?

(Asked by: username_0 on 2019-09-02)

Has anyone formalized Pollack's Dependently Typed Records in Type Theory ? Agda would be preferred, but anyone close to MLTT would work.  Weaker versions would be fine too, i.e. what Luo dubs 'dependently kinded records would be appreciated as well.
Full reference:
@Article{Pollack2002,
author="Pollack, Robert",
title="Dependently Typed Records in Type Theory",
journal="Formal Aspects of Computing",
year="2002",
month="Jul",
day="01",
volume="13",
number="3",
pages="386--402",
abstract="The language Pebble of Burstall and Lampson proposed dependent types as the underlying principle in a unified framework to explain facilities for programming in the large, such as modules and signatures, as well as for programming in the small. This proposal soon extended to large scale formal proof development as well. In fact, the functional approach to modularity has turned out to be a hard problem, which is still far from a fully satisfactory solution. This paper discusses aspects of this approach, including representations of records, informative signatures, sharing, and subtyping. My main contribution in this paper is to show that structures with dependent types and manifest fields (roughly ML style modules) are internally definable in a type theoretic framework extended with inductive-recursive definition. This shows that powerful modules follow from general principles without module-specific assumptions.",
issn="1433-299X",
doi="10.1007/s001650200018",
url="https://doi.org/10.1007/s001650200018"
}

**Tags:** dependent-type, agda

---

## 1 answers

### Answer by username_1 on 2019-09-03. Score: 2 | Accepted answer

I do not know how much of the paper it covers but we do have a module based on it in the standard library:

<https://agda.github.io/agda-stdlib/Data.Record.html>

> **Comments:**
> **username_0**: This is extremely close to what I want/need. I was hoping to internalize disjointness conditions, rather than use shadowing (as Pollack, and thus the code, does). Thus my interest in Data.List.Fresh.  
> **username_1**: By the way Fresh is nothing new, a version of it appears in Catarina Coquand's https://link.springer.com/article/10.1023/A:1019964114625 (I'll update the PR to give credits)  
> **username_0**: For my use cases, not-new is better; too many innovations at once is suspicious. But thanks for the reference.  

---

