Pith. sign in

REVIEW 43 references

Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version)

T0 review · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read Refinement kinds extend refinement types to the kind level, enabling type-safe type-level computation and meta-programming in an ML-like language, with type safety proven and a prototype built.

arxiv 1908.00441 v1 pith:73QXJBLC submitted 2019-08-01 cs.PL

Luís Caires , Bernardo Toninho This is my paper · ORCID
classification cs.PL
keywords kindtypelanguagerefinementcheckercomputationdomainjust
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

Programs often need to manipulate types and generate code, for example building database bindings from a schema. In most statically typed languages this is unsafe or requires special tools. The paper proposes adding "refinement kinds" to an ML-style language. A kind is a classifier of types, just as a type is a classifier of values. A refinement kind is a kind together with a logical condition on types, for example "record types that do not contain label l." This lets the type checker reason about the structure of types during compilation, using an SMT solver such as CVC4 to decide these conditions.

The authors define a calculus with type-level functions that can inspect and rebuild types, like records, function types, and collection types. They show how to program type-safe meta-programs: generating mutable record constructors, turning record types into XML tables, and building getter and setter wrappers. The key theorems are the standard type safety results: uniqueness of types, preservation, and progress, all proven by hand. The paper also reports a prototype type checker and interpreter.

The contribution is primarily a design: it shows that a natural extension of refinement types to the kind level is sufficient to support practical meta-programming. The work is limited to a small academic language, and the authors do not compare performance with existing languages. The main risks are the reliance on SMT solvers for decidability and the proof that type-level computation always terminates.

Extended reading notes

Core claim

This work introduces for the first time the concept of refinement kinds and illustrates how the associated discipline cleanly supports static type checking of type-level reflection, parametric and ad-hoc polymorphism. The typing and kinding disciplines allow for powerful forms of type reflection, ad-hoc polymorphism and type meta-programming. The paper validates this by establishing type safety (uniqueness, preservation, progress) and a prototype implementation that checks the examples.

Load-bearing premise

The soundness of the SMT-based entailment relation: Postulate 5.1 assumes that if the SMT validity check returns positive for the representation of a refinement formula, then the formula is valid in the intended semantics. The typing and kinding rules, including subkinding and conversion, are built on this oracle. If the encoding of types, label sets, and inductive structure in CVC4 is not faithful, the refinement logic can prove false facts about types, and type safety as stated would not follow.

Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper does not fit any parameters. It introduces a formal calculus with many new syntactic constructs, but these are part of the language design, not empirical entities. The main external assumptions are the soundness of SMT entailment, strong normalization of the type language, and the well-foundedness of the structural recursion guard.

assumptions (4)
  • domain assumption The SMT entailment relation is sound for the refinement logic (Postulate 5.1).
    Rule /e-n-t-a-i-l-s and subkinding rely on CVC4 validity; if unsound, typing can derive false refinements and break type safety. The paper explicitly assumes this.
  • domain assumption Type-level reduction is strongly normalizing.
    Claimed in Section 5 by reference to F-omega; the system adds a structural recursion operator with a syntactic guard, but no termination proof is given. It is needed for decidability of the algorithmic type checker.
  • ad hoc to paper The structural recursion guard 'structural(T,F,t)' ensures well-founded recursion.
    Rule /k-hyphen-f-i-x requires recursive calls on structurally smaller arguments; the predicate is described informally in Section 3.2. The soundness of this guard is not formalized in the paper.
  • domain assumption Extensionality and decidability results for singleton kinds carry over to this system.
    The paper bases its kind equality and equality-checking algorithm on Stone and Harper 2000/2006. If the analogy fails, kind and type equality might be undecidable or inconsistent.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version)." pith.science (2026). https://pith.science/paper/73QXJBLC

@misc{pith2026190800441,
  author       = {Pith},
  title        = {Pith review of: Refinement Kinds: Type-safe Programming with Practical Type-level Computation (Extended Version)},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/73QXJBLC}},
  note         = {Machine review of arXiv:1908.00441}
}
read the original abstract

This work introduces the novel concept of kind refinement, which we develop in the context of an explicitly polymorphic ML-like language with type-level computation. Just as type refinements embed rich specifications by means of comprehension principles expressed by predicates over values in the type domain, kind refinements provide rich kind specifications by means of predicates over types in the kind domain. By leveraging our powerful refinement kind discipline, types in our language are not just used to statically classify program expressions and values, but also conveniently manipulated as tree-like data structures, with their kinds refined by logical constraints on such structures. Remarkably, the resulting typing and kinding disciplines allow for powerful forms of type reflection, ad-hoc polymorphism and type meta-programming, which are often found in modern software development, but not typically expressible in a type-safe manner in general purpose languages. We validate our approach both formally and pragmatically by establishing the standard meta-theoretical results of type safety and via a prototype implementation of a kind checker, type checker and interpreter for our language.

Figures

Figures reproduced from arXiv: 1908.00441 by the authors.

Figure 1
Figure 1. Syntax of Kinds, Types and Refinements computing to type S if the kinds match and to U otherwise. Coupled with a term-level analogue, this enables ad-hoc polymorphism, allowing us to express non-parametric polymorphic functions. 3.1 Type-level Functions and Refinements The language of types that we have introduced up to this point essentially consists of tree-like structures with their various constructors and destr… view at source ↗
Figure 2
Figure 2. Syntax of Terms 4 A PROGRAMMING LANGUAGE WITH KIND REFINEMENTS Having covered the key details of kinding and type equality, we introduce the syntax and typing for our programming language per se, capturing the essence of an ML-style functional language with a higher-order store, the syntax of which is given in [PITH_FULL_IMAGE:figures/full_fig_p015_2.png] view at source ↗
Figure 3
Figure 3. Typing Rules Despite not knowing the exact form of the function type that is to be instantiated fort, by refining its domain and image types we can derive that t = s → Bool and give a type to applications of terms of type t correctly. Note that this is in contrast with what happens in dependent type theories such as Agda [Norell 2007] or that of Coq [CoqDevelopmentTeam 2004]), where the leveraging of dependent types… view at source ↗
Figures from the paper (1 more)
Figure 4
Figure 4. Figure 4: Operational Semantics (Excerpt) (b) If Γ ⊢ M : T and Γ, x:T, Γ ′ ⊢ N : S then Γ, Γ ′ ⊢ N{M/x} : S. Lemma 5.2 (Context Conversion). (a) Let Γ, x:T ⊢ and Γ ⊢ T ′ :: K. If Γ, x:T ⊢ J and Γ |= T ≡ T ′ :: K then Γ, x:T ′ ⊢ J. (b) Let Γ,t:K ⊢ and Γ ⊢ K ′ . If Γ,t:K ⊢ J and Γ…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

43 extracted references · 21 canonical work pages

  1. [5]

    Proceedings . 171–177. https://doi.org/10.1007/978-3-642-22110-1_14 J. Bengtson, K. Bhargavan, C. Fournet, A. D. Gordon, and S. Maffeis. 20

    doi:10.1007/978-3-642-22110-1_14

  2. [8]

    IFIP State-of-the-Art Reports: Formal Description of Programming Concepts (1991), 431–507

    Typeful Programming. IFIP State-of-the-Art Reports: Formal Description of Programming Concepts (1991), 431–507. Adam Chlipala

    work page 1991

  3. [11]

    ACM Trans

    Refinement Types for Secure Implementations. ACM Trans. Program. Lang. Syst. (2011). Cristiano Calcagno, Eugenio Moggi, and Tim Sheard

    work page 2011

  4. [13]

    InProceedings of the ACM SIGPLAN’91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, David S

    Refinement Types for ML. InProceedings of the ACM SIGPLAN’91 Conference on Programming Language Design and Implementation (PLDI), Toronto, Ontario, Canada, June 26-28, 1991, David S. Wise (Ed.). ACM, 268–277. https://doi.org/10.1145/113445.113468 Proc. ACM Program. Lang., Vol. 1, No. 1, Article . Publication dat e: August

    arXiv 1991

  5. [18]

    Logical Methods in Computer Science 14, 4 (2018)

    Reasoning with Finite Sets and Cardinality Constraints in SMT. Logical Methods in Computer Science 14, 4 (2018). https://doi.org/10.23638/LMCS-14(4:12)2018 Clark Barrett, Christopher L. Conway, Morgan Deters, Liana Hadarean, Dejan Jovanovic, Tim King, Andrew Reynolds, and Cesare Tinelli

    doi:10.23638/lmcs-14(4:12)2018 2018

  6. [19]

    In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, USA, January 21-23, 1991, David S

    A Record Calculus Bas ed on Symmetric Concatenation. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, Orlando, Florida, USA, January 21-23, 1991, David S. Wise (Ed.). ACM Press, 131–142. https://doi.org/10.1145/99583.99603 Martin Hofmann

    work page arXiv 1991

  7. [20]

    In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008

    Expressive and safe sta tic reflection with MorphJ. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008 . 79–89. Ming Kawaguchi, Patrick Maxim Rondon, and Ranjit Jhala

    work page 2008

  8. [22]

    https://doi.org/10.1145/3314221.3314630 Oleg Kiselyov, Ralf Lämmel, and Keean Schupke

    966–979. https://doi.org/10.1145/3314221.3314630 Oleg Kiselyov, Ralf Lämmel, and Keean Schupke

    arXiv

Show all 43 references
  1. [25]

    PACMPL 3, POPL (2019), 12:1–12:28

    Abstracting extensible dat a types: or, rows by any other name. PACMPL 3, POPL (2019), 12:1–12:28. https://dl.acm.org/citation.cfm?id=3290325 Ulf Norell

    2019

  2. [29]

    In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementat ion, Tucson, AZ, USA, June 7-13, 2008

    Liquid type s. In Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementat ion, Tucson, AZ, USA, June 7-13, 2008 . 159–169. John M. Rushby, Sam Owre, and Natarajan Shankar

    2008

  3. [30]

    IEEE Trans

    Subtype s for Specifications: Predicate Subtyping in PVS. IEEE Trans. Software Eng. 24, 9 (1998), 709–720. https://doi.org/10.1109/32.713327 Yannis Smaragdakis, George Balatsouras, George Kastrinis, and Mart in Bravenboer

    1998 doi

  4. [33]

    https://doi.org/10.1145/325694.325724 Christopher A

    214–227. https://doi.org/10.1145/325694.325724 Christopher A. Stone and Robert Harper

  5. [34]

    ACM Trans

    Extensional equivale nce and singleton types. ACM Trans. Comput. Log. 7, 4 (2006), 676–722. https://doi.org/10.1145/1183278.1183281 Proc. ACM Program. Lang., Vol. 1, No. 1, Article . Publication dat e: August

    2006

  6. [35]

    In Proceeding of the 16th ACM SIGPLAN international conferenc e on Functional Programming, ICFP 2011, Tokyo, Japan, Septembe r 19-21, 2011, Manuel M

    Secure dis- tributed programming with value-dependent types. In Proceeding of the 16th ACM SIGPLAN international conferenc e on Functional Programming, ICFP 2011, Tokyo, Japan, Septembe r 19-21, 2011, Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy (Eds.). ACM, 266–2...

    2011

  7. [36]

    Abstract Re finement Types. In Programming Languages and Systems - 22nd European Symposium on Programming, ESOP 2 013, Held as Part of the European Joint Con- ferences on Theory and Practice of Software, ETAPS 2013, Rom e, Italy, March 16-24,

    2013

  8. [37]

    Proceedings . 209–228. https://doi.org/10.1007/978-3-642-37036-6_13 Niki Vazou, Eric L. Seidel, Ranjit Jhala, Dimitrios Vytiniotis, and Simon L. Peyton Jones

    doi

  9. [39]

    Refinement ty pes for TypeScript. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and I mplementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery Berger (Eds.). ACM, 310–325. https://doi.org/10.1145/2908080.290...

    2016

  10. [41]

    In ACM SIG- PLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013

    System FC with explicit kind equality. In ACM SIG- PLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA - September 25 - 27, 2013 . 275–286. https://doi.org/10.1145/2500365.2500599 Hongwei Xi

    2013

  11. [43]

    In Pro- ceedings of the ACM SIGPLAN ’98 Conference on Programming La nguage Design and Implementation (PLDI), Mon- treal, Canada, June 17-19, 1998 , Jack W

    Eliminating Array Bound Checking Throug h Dependent Types. In Pro- ceedings of the ACM SIGPLAN ’98 Conference on Programming La nguage Design and Implementation (PLDI), Mon- treal, Canada, June 17-19, 1998 , Jack W. Davidson, Keith D. Cooper, and A. Michael Berman (Eds.). A CM...

    1998

  12. [44]

    P/r.sc/o.sc/o.sc/f.sc.Straightforward induction on kinding, relying on the decidabil ity of logical entailment

    51 □ L/e.sc/m.sc/m.sc/a.sc 5.7 (T/y.sc/p.sc/e.sc P/r.sc/o.sc/g.sc/r.sc/e.sc/s.sc/s.sc).If · ⊢T ::K then eitherT is a type value or T →T ′, for someT ′. P/r.sc/o.sc/o.sc/f.sc.Straightforward induction on kinding, relying on the decidabil ity of logical entailment. □ T/h.sc/e.sc...

    2019

  13. [192]

    Hall, Kevin Hammond, Simon L

    https://doi.org/10.1016/0304-3975(86)90044-7 Cordelia V. Hall, Kevin Hammond, Simon L. Peyton Jones, and Philip Wad ler

    doi

  14. [1972]

    In Proceedings of the ACM Annual Conference - Volume 2 (ACM ’72)

    Definitional Interpreters for Higher-order Programming Languages. In Proceedings of the ACM Annual Conference - Volume 2 (ACM ’72) . ACM, New York, NY, USA, 717–740. https://doi.org/10.1145/800194.805852 Patrick Maxim Rondon, Ming Kawaguchi, and Ranjit Jhala

  15. [1986]

    Theoretical Computer Science 45 (1986), 159 –

    The system F of variable types, fifteen y ears later. Theoretical Computer Science 45 (1986), 159 –

    1986

  16. [1989]

    In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programmin g Languages, Austin, Texas, USA, January 11-13, 1989

    How to Make ad-hoc Polymo rphism Less ad-hoc. In Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programmin g Languages, Austin, Texas, USA, January 11-13, 1989 . 60–76. https://doi.org/10.1145/75277.75283 Stephanie Weirich, Justin Hsu, and Richard A. ...

    1989

  17. [1991]

    ACM Trans

    Dynamic Typing in a Statically Typed Language. ACM Trans. Program. Lang. Syst. 13, 2 (1991), 237–268. https://doi.org/10.1145/103135.103138 Thorsten Altenkirch and Conor McBride

    1991

  18. [1996]

    ACM Trans

    Type Classes in Haskell. ACM Trans. Program. Lang. Syst. 18, 2 (1996), 109–138. https://doi.org/10.1145/227699.227700 Robert Harper and Benjamin C. Pierce

    1996

  19. [1998]

    In Automata, Languages and Pro- gramming, 25th International Colloquium, ICALP’98, Aalbo rg, Denmark, July 13-17, 1998, Proceedings

    Structural Recursive Definitions in Type Theo ry. In Automata, Languages and Pro- gramming, 25th International Colloquium, ICALP’98, Aalbo rg, Denmark, July 13-17, 1998, Proceedings . 397–408. https://doi.org/10.1007/BFb0055070 Jean-Yves Girard

    1998 doi

  20. [1999]

    https://doi.org/10.1145/331960.331977 J

    109–122. https://doi.org/10.1145/331960.331977 J. Garrett Morris and James McKinna

  21. [2000]

    In POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Pr ogramming Languages, Boston, Massachusetts, USA, January 19-21,

    Deciding Type Equivalence with Singleton Kinds. In POPL 2000, Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Pr ogramming Languages, Boston, Massachusetts, USA, January 19-21,

    2000

  22. [2002]

    Generic Programming within Dependently Typed Programming. In Generic Programming, IFIP TC2/WG2.1 Working Conference on Generic Programming, July 11-12, 2002, Dagstuhl, Germany (IFIP Conference Proceedings), Jeremy Gibbons and Johan Jeuring (Eds.), Vol

    2002

  23. [2003]

    Closed types for a safe imperative MetaML. J. Funct. Program. 13, 3 (2003), 545–571. https://doi.org/10.1017/S0956796802004598 Luca Cardelli

    2003 doi

  24. [2004]

    In Proceed- ings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Sn owbird, UT, USA, September 22-22, 2004

    Strongly t yped heterogeneous collections. In Proceed- ings of the ACM SIGPLAN Workshop on Haskell, Haskell 2004, Sn owbird, UT, USA, September 22-22, 2004 . 96–107. https://doi.org/10.1145/1017472.1017488 Daan Leijen and Erik Meijer

    2004

  25. [2006]

    In Gen- erative Programming and Component Engineering, 5th Intern ational Conference, GPCE 2006, Portland, Oregon, USA, October 22-26, 2006, Proceedings , Stan Jarzabek, Douglas C

    Reflectiv e program generation with patterns. In Gen- erative Programming and Component Engineering, 5th Intern ational Conference, GPCE 2006, Portland, Oregon, USA, October 22-26, 2006, Proceedings , Stan Jarzabek, Douglas C. Schmidt, and Todd L. Veldhuizen (Eds .). ACM, 275–2...

    2006

  26. [2007]

    Dependent ML An approach to practical programming with dependent types. J. Funct. Program. 17, 2 (2007), 215–286. https://doi.org/10.1017/S0956796806006216 Hongwei Xi and Frank Pfenning

    2007 doi

  27. [2008]

    In Tools and Algorithms for the Construction and Analysis of Systems, 14th International C onference, TACAS 2008, (Lecture Notes in Computer Science) , C

    Z3: An Efficient S MT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International C onference, TACAS 2008, (Lecture Notes in Computer Science) , C. R. Ramakrishnan and Jakob Rehof (Eds.), Vol

    2008

  28. [2009]

    Type-bas ed data structure verification. In Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Des ign and Implementation, PLDI 2009, Dublin, Ireland, June 15-21, 2009, Michael Hind and Amer Diwan (Eds.). ACM, 304–315. https://doi.org/10.1145/1542476.1542510...

    2009

  29. [2010]

    In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and I mplementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, Benjamin G

    Ur: statically-typed metaprogramming with type-level record computation. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and I mplementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, Benjamin G. Zorn and Alexander Aiken (Eds.). ACM...

    2010

  30. [2011]

    In Computer Aided Verification - 23rd International Conference, CA V 2011, Snowbird, UT, USA, July 14-20,

    CVC4. In Computer Aided Verification - 23rd International Conference, CA V 2011, Snowbird, UT, USA, July 14-20,

    2011

  31. [2013]

    Proceedings . 377–391. https://doi.org/10.1007/978-3-642-38574-2_26 John C. Reynolds

    doi

  32. [2014]

    In Proceedings of the 19th ACM SIGPLAN international conferen ce on Functional programming, Gothenburg, Sweden, September 1-3, 2014 , Johan Jeuring and Manuel M

    Refinement types for Haskell. In Proceedings of the 19th ACM SIGPLAN international conferen ce on Functional programming, Gothenburg, Sweden, September 1-3, 2014 , Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 269–282 . https://doi.org/10.1145/2628136.2628161 Panagiot...

    2014

  33. [2015]

    In Programming Languages and Systems - 13th Asian Symposium, A PLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings

    More Sound Static Handling of Java Reflection. In Programming Languages and Systems - 13th Asian Symposium, A PLAS 2015, Pohang, South Korea, November 30 - December 2, 2015, Proceedings . 485–503. Christopher A. Stone and Robert Harper

    2015

  34. [2019]

    In Proceedings of the 40th ACM SIGPLAN Conference on Programmi ng Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 20

    Type-level compu- tations for Ruby libraries. In Proceedings of the 40th ACM SIGPLAN Conference on Programmi ng Language Design and Implementation, PLDI 2019, Phoenix, AZ, USA, June 22-26, 20

    2019

  35. [4963]

    https://doi.org/10.1007/978-3-540-78800-3_24 Manuel Fähndrich, Michael Carbin, and James R

    Springer, 337–340. https://doi.org/10.1007/978-3-540-78800-3_24 Manuel Fähndrich, Michael Carbin, and James R. Larus

    doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.