2026-03-06 01:00:09
2 DEPENDENTLY-TYPED OBJECT-ORIENTED PROGRAMMING
4 DESIGN CONSTRAINTS AND SOLUTIONS
\
Codata types. Codata types were first introduced by Hagino [Hagino 1987, 1989]. The original interpretation of codata types stems from coalgebras in category theory. An overview of the history of codata types as coalgebras is given by Setzer [Setzer 2012]. We have discussed the relation between codata types and OOP in Section 1.1. The expression problem. The expression problem poses the challenge for statically typed languages to create a type which can be extended by both new producers and new consumers. Based on earlier observations, Wadler [1998] formulated the problem and gave it its current name.
\ The expression problem for proofs is recognized as an important challenge in the verification community, but there are fewer proposed and implemented solutions than in the programming world. One popular solution in the programming world is Swierstra [2008]’s “Data Types à la carte” approach. In that approach, a type is defined as the fixpoint of a coproduct of functors which can be extended by new functors in a modular way. Most proposed solutions for dependent types are based on Swierstra [2008]’s approach and extend them to dependent types. Delaware et al. [2013a,b]; Delaware [2013] as well as Keuchel and Schrijvers [2013] implemented this approach for the Coq proof assistant and Schwaab and Siek [2013] implemented it for Agda.
\ A system for writing modular proofs in the Isabelle proof assistant has been described by Molitor [2015]. The most recent adaptation of the idea is by Forster and Stark [2020], who give an excellent presentation of this line of work in their related work section. In this article, our focus was not to propose a solution to the expression problem for proofs, since the defunctionalization and refunctionalization algorithms are whole-program transformations. Instead, our approach distills the essence of the expression problem for dependent types: Neither the functional nor the object-oriented decomposition solves the expression problem, since data types cannot be easily extended by new constructors, and codata types cannot be easily extended by new destructors.
\
Dependently-typed object-oriented programming. In Section 2 we presented our perspective on dependently-typed object-oriented programming. But we are not the first to think about this design space. Jacobs [1995] proposes using coalgebras to express object-oriented classes with coalgebraic specifications. His concept is based on three main components: objects, class implementations, and class specifications. The latter are used to specify a set of methods on an abstract state space as well as a set of assertions that define the behavior of these methods. Such a specification can then be implemented by a class.
\ A class gives a carrier set as a concrete interpretation for the state space and a coalgebra that implements the specified methods. An object is then just an element of the carrier set. In our system, we can express specifications similar to Jacobs’ proposal using self-parameters on destructors (see Section 2.2). Rather than having separate notions of specifications, classes, and objects, our system has a singular notion of codata types. Jacobs separates these notions to construct a model in which objects are indistinguishable if they are bisimilar according to their specification.
\ In contrast, in our system, we have a full syntactic duality between data and codata types through de- and refunctionalization. Hence, we need to decouple codata types from the semantics that are usually associated with them, including behavioral equality such as bisimilarity. Setzer [2006] conceived of dependently-typed object-oriented programming by specifying interfaces and having interactive programs as objects implementing these interfaces. The interfaces contain a command type, which represents the method signatures of an interface. Interactive programs are programs that react to incoming method calls by producing a return value and a new object.
\
Dependent type theories with definable Π-type and Σ-type. In Section 2.3 we demonstrated that the programmer can define both the Π-type and the Σ-type in our system, whereas in most proof assistants only the Σ-type can be defined. This is a generalization of the observation that programmers can’t define the function type in most functional programming languages, but that the function type can be defined in object-oriented languages [Setzer 2003]. Apart from this paper, the only other dependent type theory that doesn’t presuppose a built-in Π-type is by Basold [2018]; Basold and Geuvers [2016]. Like us, they give an explicit definition of the Π-type in their system.
\ Their definition, however, is slightly different from ours, since they have a more expressive core system. In their system, parameterized type constructors and type variables don’t have to be fully applied. Partially applied type constructors have a special type Γ _ ∗, and they specify a sort of simply-typed lambda calculus which governs the rules for abstracting over, and partially applying type constructors to arguments. As a result, their definition of the Π and Σ-type is a bit simpler: We have to use a previously-defined non-dependent function type 𝐴 → Type to represent the type family that the Σ and Π-types are indexed over, while they use a partially applied type variable 𝑋 : 𝐴 _ ∗. Our system is also not consistent; theirs is, and they prove both subject reduction and strong normalization.
\
Dependent pattern matching. The traditional primitive elimination forms in dependent type theories are eliminators. The eliminator for natural numbers, for example, has the type ∀(P : N → Type), P 0 → (∀n : N, P n → P (S n)) → ∀n : N, P n. They are suitable for studying the metatheory of dependent types, but programming with them isn’t very ergonomic. A more convenient alternative to eliminators is dependent pattern matching, a generalization of ordinary pattern matching to dependent types, which was first proposed by Coquand [1992].
\ While ordinary pattern matching can be compiled to eliminators and is therefore nothing more than syntactic sugar, the compilation of dependent pattern matches additionally requires Streicher [1993]’s axiom K. Hofmann and Streicher [1994] proved that this axiom does not follow from the standard elimination rules for the identity type. Since the K axiom is sometimes undesirable—it is incompatible with other principles such as univalence—a variant of dependent pattern matching which does not rely on axiom K was developed by Cockx et al. [2014]. We use a variant of dependent pattern and copattern matching which requires axiom K if we want to compile it to eliminators, but we could get rid of this dependency by applying the three restrictions presented in Cockx’ thesis [Cockx 2017, p.55].
\
Copattern matching. Copattern matching as a dual concept to pattern matching was first proposed by Abel et al. [2013]. Their work was motivated by the deficiencies of previous approaches which used constructors to represent infinite objects. For instance, the coinductive types originally introduced in Coq broke subject reduction, as noted by Giménez [1996] and Oury [2008]. Even simple infinite objects such as streams cannot be represented using constructors and pattern matching in a sensible way. This follows from the observation of Berger and Setzer [2018] that there exists no decidable equality for streams which admits a one-step expansion of a stream 𝑠 to a stream (cons 𝑛 𝑠′ ).
\
Inconsistent dependent type theories. The type theory presented in this paper is inconsistent, i.e. every type is inhabited by some term, a property it shares with most programming languages but not with proof assistants. However, the inconsistency of the theory does not imply that the properties expressed by the dependent types are meaningless. We can compare the situation to the programming language Haskell, where it is already possible to write dependent programs by using several language extensions and programming tricks [Eisenberg and Weirich 2012; Lindley and McBride 2013].
\ Instead of relying on these tricks, a more ergonomic and complete design of dependent types in Haskell has been the subject of various articles [Weirich et al. 2019, 2017] and PhD theses [Eisenberg 2016; Gundry 2013]. Their main insight also applies to our system: the central property of an inconsistent dependent type theory is type soundness [Wright and Felleisen 1994]. For example, every term of type Vec(5) can only evaluate to a vector containing five elements or diverge; it cannot evaluate to a vector of six elements. But they also show that inconsistency has downsides, especially for optimization: In a consistent theory every term of type Eq(𝑠, 𝑡) must evaluate to the term refl, and can therefore be erased during compilation. In an inconsistent theory, we cannot erase the equality witness, since we could otherwise write a terminating unsafe coercion between arbitrary types, which would violate type soundness.
\
Defunctionalization and refunctionalization. The related work on defunctionalization and refunctionalization can be partitioned into two groups: The first group only considers defunctionalization and refunctionalization for the function type, while the second group generalizes them to transformations between arbitrary data and codata types. De/Refunctionalization of the function type has a long history, which starts with the seminal paper by Reynolds [1972] and the later work of Danvy and Millikin [2009]; Danvy and Nielsen [2001]. That the defunctionalization of polymorphic functions requires GADTs was first observed by Pottier and Gauthier [2006].
\ In a recent paper, Huang and Yallop [2023] describe the defunctionalization of dependent functions, and especially how to correctly deal with type universes and positivity restrictions, but don’t consider the general case of indexed data and codata types. On the contrary, they do not use data types at all and instead introduce the construct of first-class function labels which enables them to avoid problems arising from the expressivity of data type definitions like recursive types. The generalization of defunctionalization from functions to arbitrary codata types was first described by Rendel et al. [2015] for a simply typed system without local lambda abstractions or local pattern matches.
\ That the generalization to polymorphic data and codata types then also requires GAcoDTs has been described by Ostermann and Jabs [2018]. How to treat local pattern and copattern matches in such a way as to preserve the invertibility of defunctionalization and refunctionalization has been described by Binder et al. [2019]. Recently, Zhang et al. [2022] implemented defunctionalization and refunctionalization for the programming language Scala, and used these transformations for some larger case studies. In this article, we describe the generalization to indexed data and codata types, but in distinction to Huang and Yallop [2023] we circumvent the problems of type universes and positivity restrictions by working in an inconsistent type theory.
\
Most dependently typed programming languages don’t support programming with codata as well as programming with data. The main reason some proof assistants support codata types at all was that some support was necessary for the convenient formalization of theorems about infinite and coalgebraic objects. But codata types are useful for more than just representing infinite objects like streams; they represent an orthogonal way to structure programs and proofs, with different extensibility properties and reasoning principles.
\ In this paper we have presented a vision of how programming can look in a dependently typed language in which the data and codata sides are completely symmetric and treated with equal care. By implementing this language and testing it on a case study we have demonstrated that this style of purely functional, dependently typed object-oriented programming does work. We think that this way of systematic language design, in place of ad-hoc extensions, provides a good case study on how the design of dependently typed languages and proof assistants should be approached.
\ DATA-AVAILABILITY STATEMENT
This article is accompanied by an online IDE available at polarity-lang.github.io/oopsla24 where the examples discussed in this paper can be selected and loaded. This online IDE consists of a static website hosted on GitHub pages, with all the code running in the browser on the client side. Should the hosted website despite our best efforts no longer be available, then it is possible to recreate it locally using the archived version available at Zenodo [Binder et al. 2024].
\
Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. 2013. Copatterns: Programming Infinite Structures by Observations. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Rome, Italy) (POPL ’13). Association for Computing Machinery, New York, NY, USA, 27–38. https://doi.org/ 10.1145/2480359.2429075
\ Thorsten Altenkirch and Conor McBride. 2006. Towards Observational Type Theory. http://www.strictlypositive.org/ott. pdf Henning Basold. 2018. Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic. Ph. D. Dissertation. Radboud University. https://hdl.handle.net/2066/190323
\ Henning Basold and Herman Geuvers. 2016. Type Theory Based on Dependent Inductive and Coinductive Types. In Proceedings of the Symposium on Logic in Computer Science (New York). Association for Computing Machinery, New York, NY, USA, 327–336. https://doi.org/10.1145/2933575.2934514 Ulrich Berger and Anton Setzer. 2018. Undecidability of Equality for Codata Types. In Coalgebraic Methods in Computer Science, Corina Cîrstea (Ed.). Springer, 34–55. https://doi.org/10.1007/978-3-030-00389-0_4
\ David Binder, Julian Jabs, Ingo Skupin, and Klaus Ostermann. 2019. Decomposition Diversity with Symmetric Data and Codata. Proc. ACM Program. Lang. 4, POPL, Article 30 (2019), 28 pages. https://doi.org/10.1145/3371098
\ David Binder, Ingo Skupin, Tim Süberkrüb, and Klaus Ostermann. 2024. Deriving Dependently-Typed OOP from First Principles. https://doi.org/10.5281/zenodo.10779424 Archived version of the submitted artefact.
\ Ranald Clouston, Aleš Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. 2017. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science 12 (April 2017). Issue 3. https://doi.org/10.2168/LMCS-12(3:7)2016
\ Jesper Cockx. 2017. Dependent Pattern Matching and Proof-Relevant Unification. Ph. D. Dissertation. KU Leuven.
\ Jesper Cockx, Dominique Devriese, and Frank Piessens. 2014. Pattern Matching without K. In International Conference on Functional Programming. Association for Computing Machinery, New York, NY, USA, 257–268. https://doi.org/10.1145/ 2628136.2628139
\ William R. Cook. 1990. Object-Oriented Programming versus Abstract Data Types. In Proceedings of the REX Workshop / School on the Foundations of Object-Oriented Languages. Springer, 151–178. https://doi.org/10.1007/BFb0019443
\ William R. Cook. 2009. On Understanding Data Abstraction, Revisited. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications: Onward! Essays (Orlando). Association for Computing Machinery, New York, NY, USA, 557–572. https://doi.org/10.1145/1640089.1640133
\ Thierry Coquand. 1992. Pattern Matching With Dependent Types. In Proceedings of the 1992 Workshop on Types for Proofs and Programs (Bastad, Sweden), Bengt Nordström, Kent Pettersson, and Gordon Plotkin (Eds.). 66–79.
\ Olivier Danvy and Kevin Millikin. 2009. Refunctionalization at Work. Science of Computer Programming 74, 8 (2009), 534–549. https://doi.org/10.1016/j.scico.2007.10.007
\ Olivier Danvy and Lasse R. Nielsen. 2001. Defunctionalization at Work. In Proceedings of the Conference on Principles and Practice of Declarative Programming (Florence). 162–174. https://doi.org/10.1145/773184.773202
\ Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2013a. Meta-Theory à La Carte. In Symposium on Principles of Programming Languages (Rome) (POPL ’13). Association for Computing Machinery, New York, NY, USA, 207–218. https://doi.org/10.1145/2429069.2429094
\ Benjamin Delaware, Steven Keuchel, Tom Schrijvers, and Bruno C.d.S. Oliveira. 2013b. Modular Monadic Meta-Theory. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming (Boston, Massachusetts, USA) (ICFP ’13). Association for Computing Machinery, New York, NY, USA, 319–330. https://doi.org/10.1145/2500365. 2500587
\ Benjamin James Delaware. 2013. Feature Modularity in Mechanized Reasoning. Ph. D. Dissertation. The University of Texas at Austin. Paul Downen, Zachary Sullivan, Zena M. Ariola, and Simon Peyton Jones. 2019. Codata in Action. In European Symposium on Programming (ESOP ’19). Springer, 119–146. https://doi.org/10.1007/978-3-030-17184-1_5
\ Richard Eisenberg. 2016. Dependent Types in Haskell: Theory and Practice. Ph. D. Dissertation. University of Pennsylvania.
\ Richard A. Eisenberg, Guillaume Duboc, Stephanie Weirich, and Daniel Lee. 2021. An Existential Crisis Resolved: Type Inference for First-Class Existential Types. Proc. ACM Program. Lang. 5, ICFP, Article 64 (aug 2021), 29 pages. https: //doi.org/10.1145/3473569
\ Richard A. Eisenberg and Stephanie Weirich. 2012. Dependently Typed Programming with Singletons. In Proceedings of the Haskell Symposium (Copenhagen, Denmark) (Haskell ’12). Association for Computing Machinery, New York, NY, USA, 117–130. https://doi.org/10.1145/2364506.2364522
\ Matthias Felleisen and Robert Hieb. 1992. The Revised Report on the Syntactic Theories of Sequential Control and State. Theoretical Computer Science 103, 2 (1992), 235–271. https://doi.org/10.1016/0304-3975(92)90014-7
\ Yannick Forster and Kathrin Stark. 2020. Coq à La Carte: A Practical Approach to Modular Syntax with Binders. In Proceedings of the Conference on Certified Programs and Proofs (New Orleans) (CPP 2020). Association for Computing Machinery, New York, NY, USA, 186–200. https://doi.org/10.1145/3372885.3373817
\ Peng Fu and Aaron Stump. 2014. Self Types for Dependently Typed Lambda Encodings. In International Conference on Rewriting Techniques and Applications, Gilles Dowek (Ed.). Springer, 224–239. https://doi.org/10.1007/978-3-319-08918- 8_16
\ Erich Gamma, Richard Helm, Ralph Johnson, and John Vlissides. 1995. Design Patterns: Elements of Reusable Object-Oriented Software.
Addison-Wesley Publishing Co., Boston.
\ Richard Garner. 2009. On the Strength of Dependent Products in the Type Theory of Martin-Löf. Annals of Pure and Applied Logic 160, 1 (2009), 1–12. https://doi.org/10.1016/j.apal.2008.12.003
\ Herman Geuvers. 2001. Induction Is Not Derivable in Second Order Dependent Type Theory. In Typed Lambda Calculi and Applications, Samson Abramsky (Ed.). Springer, Berlin, Heidelberg, 166–181. https://doi.org/3-540-45413-6_16
\ Herman Geuvers. 2014. The Church-Scott Representation of Inductive and Coinductive Data. https://www.cs.vu.nl/ ~femke/courses/ep/slides/herman-data-types.pdf Presented at the TYPES 2014 meeting.
\ Eduardo Giménez. 1996. Un Calcul de Constructions Infinies et son application a la vérification de systemes communicants. Ph. D. Dissertation. Lyon, École normale supérieure (sciences).
\ Jean-Yves Girard. 1972. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. Thése de Doctorat d’Etat. Université de Paris VII.
\ Brian Goetz et al. 2014. JSR 335: Lambda Expressions for the Java Programming Language. https://jcp.org/en/jsr/detail?id= 335
\ Adam Gundry. 2013. Type Inference, Haskell and Dependent Types. Ph. D. Dissertation. University of Strathclyde.
\ Tatsuya Hagino. 1987. A Categorical Programming Language. Ph. D. Dissertation. University of Edinburgh. https://doi. org/10.48550/arXiv.2010.05167
\ Tatsuya Hagino. 1989. Codatatypes in ML. Journal of Symbolic Computation 8, 6 (1989), 629–650. https://doi.org/10.1016/ S0747-7171(89)80065-3
\ Martin Hofmann. 1997. Syntax and Semantics of Dependent Types. In Extensional Constructs in Intensional Type Theory. Springer, London, 13–54. https://doi.org/10.1007/978-1-4471-0963-1_2
\ Martin Hofmann and Thomas Streicher. 1994. The Groupoid Model Refutes Uniqueness of Identity Proofs. In Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science. IEEE, 208–212. https://doi.org/10.1109/LICS.1994.316071
\ William Alvin Howard. 1980. The Formulae-as-Types Notion of Construction. In To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism, Haskell Curry, Hindley B., Seldin J. Roger, and P. Jonathan (Eds.). Academic Press.
\ Yulong Huang and Jeremy Yallop. 2023. Defunctionalization with Dependent Types. Proc. ACM Program. Lang. 7, PLDI, Article 127 (jun 2023), 23 pages. https://doi.org/10.1145/3591241
\ Antonius J. C. Hurkens. 1995. A Simplification of Girard’s Paradox. In Proceedings of the Conference on Typed Lambda Calculi and Applications. Springer, London, 266–278. http://dx.doi.org/10.1007/BFb0014058
\ Bart Jacobs. 1995. Objects and Classes, Coalgebraically. In Object Orientation with Parallelism and Persistence, Burkhard Freitag, Cliff B. Jones, Christian Lengauer, and Hans-Jörg Schek (Eds.). Springer, 83–103. https://doi.org/10.1007/978- 1-4613-1437-0_5
\ Steven Keuchel and Tom Schrijvers. 2013. Generic Datatypes à La Carte. In Workshop on Generic Programming (Boston) (WGP ’13). Association for Computing Machinery, New York, NY, USA, 13–24. https://doi.org/10.1145/2502488.2502491
\ Pieter Koopman, Rinus Plasmeijer, and Jan Martin Jansen. 2014. Church Encoding of Data Types Considered Harmful for Implementations: Functional Pearl. In Proceedings of the 26nd 2014 International Symposium on Implementation and Application of Functional Languages (IFL ’14). Association for Computing Machinery, New York, NY, USA, Article 4, 12 pages. https://doi.org/10.1145/2746325.2746330
\ Sam Lindley and Conor McBride. 2013. Hasochism: The Pleasure and Pain of Dependently Typed Haskell Programming. In Proceedings of the Haskell Symposium (Boston) (Haskell ’13). Association for Computing Machinery, New York, NY, USA, 81–92. https://doi.org/10.1145/2503778.2503786 Richard Molitor. 2015. Open Inductive Predicates. Master’s thesis. Karlsruher Institut für Technologie (KIT).
\ Hiroshi Nakano. 2000. A Modality for Recursion. In Proceedings of the Symposium on Logic in Computer Science. 255–266. https://doi.org/10.1109/LICS.2000.855774
\ Klaus Ostermann and Julian Jabs. 2018. Dualizing Generalized Algebraic Data Types by Matrix Transposition. In European Symposium on Programming. Springer, 60–85. https://doi.org/10.1007/978-3-319-89884-1_3
\ Nicolas Oury. 2008. Coinductive Types and Type Preservation. Message on the coq-club mailing list (2008). https://sympa. inria.fr/sympa/arc/coq-club/2008-06/msg00022.html
\ François Pottier and Nadji Gauthier. 2006. Polymorphic Typed Defunctionalization and Concretization. Higher-Order and Symbolic Computation 19, 1 (3 2006), 125–162. https://doi.org/10.1007/s10990-006-8611-7
\ Tillmann Rendel, Julia Trieflinger, and Klaus Ostermann. 2015. Automatic Refunctionalization to a Language with Copattern Matching: With Applications to the Expression Problem. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming (Vancouver, BC, Canada) (ICFP 2015). Association for Computing Machinery, New York, NY, USA, 269–279. https://doi.org/10.1145/2784731.2784763
\ John Charles Reynolds. 1972. Definitional Interpreters for Higher-Order Programming Languages. In ACMConf (Boston). Association for Computing Machinery, New York, NY, USA, 717–740. https://doi.org/10.1145/800194.805852
\ Christopher Schwaab and Jeremy G. Siek. 2013. Modular Type-Safety Proofs in Agda. In Proceedings of the 7th Workshop on Programming Languages Meets Program Verification (Rome, Italy) (PLPV ’13). Association for Computing Machinery, New York, NY, USA, 3–12. https://doi.org/10.1145/2428116.2428120
\ Anton Setzer. 2003. Java as a Functional Programming Language. In Types for Proofs and Programs, Herman Geuvers and Freek Wiedijk (Eds.). Springer, Berlin, Heidelberg, 279–298. https://doi.org/10.1007/3-540-39185-1_16
\ Anton Setzer. 2006. Object-Oriented Programming in Dependent Type Theory. Trends in Functional Programming 7 (2006), 91–108.
\ Anton Setzer. 2012. Coalgebras as Types Determined by Their Elimination Rules. In Epistemology versus Ontology. Essays on the Philosophy and Foundations of Mathematics in Honour of Per Martin-Löf, Peter Dybjer, Sten Lindström, Erik Palmgren, and Göran Sundholm (Eds.). Logic, Epistemology, and the Unity of Science, Vol. 27. Springer, Dordrecht, 351–369. https: //doi.org/10.1007/978-94-007-4435-6_16
\ Thomas Streicher. 1993. Investigations into Intensional Type Theory. Habilitationsschrift, Ludwig-Maximilians-Universität München. Wouter Swierstra. 2008. Data Types à la Carte. Journal of Functional Programming 18, 4 (2008), 423–436. https://doi.org/ 10.1017/S0956796808006758
\ Neil Tennant. 1982. Proof and Paradox. Dialectica 36, 2-3 (1982), 265–296. https://doi.org/10.1111/j.1746-8361.1982.tb00820.
\ x David Thibodeau, Andrew Cave, and Brigitte Pientka. 2016. Indexed Codata Types. In Proceedings of the International Conference on Functional Programming (Nara, Japan) (ICFP 2016). Association for Computing Machinery, New York, NY, USA, 351–363. https://doi.org/10.1145/2951913.2951929
\ Philip Wadler. 1998. The Expression Problem. (11 1998). https://homepages.inf.ed.ac.uk/wadler/papers/expression/ expression.txt Note to Java Genericity mailing list. S
\ tephanie Weirich, Pritam Choudhury, Antoine Voizard, and Richard A. Eisenberg. 2019. A Role for Dependent Types in Haskell. Proc. ACM Program. Lang. 3, ICFP, Article 101 (jul 2019), 29 pages. https://doi.org/10.1145/3341705
\ Stephanie Weirich, Antoine Voizard, Pedro Henrique Azevedo de Amorim, and Richard A. Eisenberg. 2017. A Specification for Dependent Types in Haskell. Proceedings of the ACM on Programming Languages 1, ICFP (8 2017). https://doi.org/ 10.1145/3110275
\ Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Information and Computation 115, 1 (11 1994), 38–94. https://doi.org/10.1006/inco.1994.1093
\ Weixin Zhang, Cristina David, and Meng Wang. 2022. Decomposition Without Regret. arXiv preprint arXiv:2204.10411 (2022). https://doi.org/10.48550/ARXIV.2204.10411
\
:::info Authors:
:::
:::info This paper is available on arxiv under CC 4.0 license.
:::
\
2026-03-06 01:00:03
We spent four months building self-serve analytics. Then I watched people actually try to use it.
\ I'll be honest about what prompted this. It wasn't intellectual curiosity. It was a Jira ticket.
\ The ticket said: "Dashboard not working." I opened it expecting a broken filter or a missing data refresh. Instead, I found a three-paragraph message from a product manager explaining that she had been staring at the dashboard for twenty minutes and still couldn't figure out whether her feature launch had been successful.
\ The dashboard was working perfectly. Every chart is loaded. Every filter responded. The data was fresh, accurate, and well-modeled. I had built it myself, and I was proud of it.
\ She still couldn't answer her question.
\ That ticket sat in my head for weeks. Eventually, I decided to do something I'd never done before. I took one of our most-used dashboards and watched five different teams try to use it for a real decision. Not a demo. Not a training session. A real question they actually needed answered that week.
The dashboard was our product engagement summary. It had daily active users, feature adoption rates, retention curves, and a handful of revenue-adjacent metrics. It was built in Looker, connected to a well-tested dbt model, refreshed every four hours. By every engineering standard, it was solid work.
\ I picked five teams that regularly accessed this dashboard according to our usage logs. Each team had a question they were actively trying to answer.
\ Product wanted to know if a recent onboarding redesign had improved activation.
\ Marketing wanted to know which channels were driving the highest-value users.
\ Customer Success wanted to know which accounts were showing early churn signals.
\ Sales wanted to know if usage patterns correlated with upsell readiness.
\ Finance wanted to know if the per-user cost trend was sustainable at the current growth.
\ Same dashboard. Same data. Five real questions from five real teams, all due that week.
\ I asked each team if I could sit with them (or join their video call) while they worked through their question using the dashboard. No coaching, no hints. I just wanted to watch.
\ I'll admit my bias upfront. I expected at least three of the five to get what they needed. I had built this dashboard with cross-functional use in mind. I had added context descriptions to every chart. I had even written a short how-to doc that nobody, as it turned out, had read.
The product team spent the first eight minutes trying to isolate their onboarding cohort. The dashboard had a date filter and a feature filter, but no cohort filter. They needed to compare users who signed up before the redesign with users who signed up after it. The dashboard couldn't do this without a workaround.
\ The PM opened a SQL editor in a separate tab. She wrote a query to pull user IDs by signup date, then tried to paste them into the dashboard filter. The filter had a 100-value limit. Her cohort had 4,200 users.
\ She gave up and Slacked me, asking for a custom cut of the data. Total time on the dashboard: fourteen minutes. Decision made from the dashboard: none.
Marketing had the most interesting failure because they technically found what they were looking for. The dashboard showed acquisition channel breakdowns. They could see that paid social was driving the most new users. They concluded that paid social was their best-performing channel and started drafting a budget reallocation proposal.
\ The problem: the dashboard showed volume, not value. Paid social had the most users but the lowest retention rate (which was visible on a different tab; they didn't click) and the lowest average contract value (which was on a different dashboard entirely). Their "best" channel was actually their most expensive per retained dollar.
\ They made a decision. It was the wrong one. I flagged it after the session. They were grateful but also frustrated. "Why doesn't the dashboard just show us which channel is best?" one of them asked.
\ Because "best" means something different to every team. The dashboard showed metrics. It didn't show answers. That's a design philosophy we'll come back to.
Customer Success was the team that actually succeeded, and it's worth understanding why.
\ Their lead had spent three months building a mental model of what early churn looks like. She knew the specific combination of signals: declining weekly logins, no feature adoption beyond the core workflow, and support ticket frequency above a threshold. She didn't need the dashboard to tell her the answer. She needed it to confirm what she already suspected.
\ She opened the dashboard, filtered to her accounts, checked three charts in sequence, and said, "Yep, these four accounts need intervention calls this week." Total time: six minutes.
\ The dashboard worked for her because she already knew what to look for and how to read the signals together. She was interpreting, not just reading.
Sales spent twelve minutes on the dashboard and then asked me a question that I still think about: "Can you just tell me which accounts to call?"
\ They wanted a ranked list. The dashboard gave them dimensions and measures. They could see usage trends per account, but translating "this account's usage went up 40% last month" into "this account is ready for an upsell conversation" required context that the dashboard didn't have. It didn't know the contract renewal date, the existing plan tier, or whether the account had already been contacted.
\ The sales rep was polite about it. She said the dashboard was "interesting", which is the business equivalent of "I will never open this again."
Finance didn't use the dashboard. They exported the underlying data to a spreadsheet within the first two minutes. When I asked why, the answer was straightforward: "I need to build a model, not look at a chart."
\ They needed to run scenarios. What happens to per-user cost at 20% growth versus 40% growth? What's the breakeven point? The dashboard showed the current state. Finance needed to manipulate the inputs. A static visualization, no matter how accurate, cannot be a planning tool.
\ I don't count this as a dashboard failure. It's a use case mismatch. But it raises a question about whether we should have built this team a spreadsheet template instead of a dashboard tab. We didn't ask. We assumed everyone wants dashboards.
| Team | Found relevant data? | Answered their question? | Made a decision? | Time spent | |----|----|----|----|----| | Product | Partially | No | No | 14 min | | Marketing | Yes | Yes (incorrectly) | Yes (wrong one) | 18 min | | Customer Success | Yes | Yes | Yes | 6 min | | Sales | Partially | No | No | 12 min | | Finance | Yes | N/A (wrong format) | No | 2 min |
The most dangerous outcome is a confident wrong answer. Marketing's experience scared me more than any other. The dashboard gave them data. They interpreted the data. They concluded. The conclusion was wrong because the dashboard showed an incomplete picture, and they had no reason to suspect it was incomplete. A dashboard that gives you a wrong answer, you believe, is worse than a dashboard that gives you nothing at all. At least "I don't know" doesn't trigger a budget reallocation.
\ The gap between metrics and decisions is enormous. Every team came in with a question. Not one of those questions could be answered by a single chart. Decisions require combining multiple signals, applying business context, and making a judgment call. Dashboards show metrics. The translation from metrics to decisions happens entirely in the human's head, and most dashboards give that translation process zero support.
\ Domain expertise is the real filter. Customer Success succeeded because of their lead's experience, not because of the dashboard's design. She knew what to look for. Everyone else was browsing, hoping the right insight would jump out. Self-serve analytics assumes domain expertise that most teams haven't built yet. We ship the tool before we teach the thinking.
\ Nobody reads the documentation. I wrote context descriptions. I wrote a how-to guide. I added tooltip explanations to every metric. The usage data shows that zero people (not low, zero) clicked on the metric descriptions in the past quarter. People don't read inline documentation in dashboards for the same reason they don't read terms of service. They came to do something, not to learn something.
\ The teams that export to spreadsheets aren't doing it wrong. Finance's instinct to export was the most rational response to their actual need. We treat spreadsheet exports as a failure of our BI layer. Maybe it's actually a signal that some users need interactive, manipulable data rather than curated visualizations. Building a dashboard for someone who needs a spreadsheet is like building a report for someone who needs a conversation.
\ "Self-serve" is a spectrum, not a switch. Customer Success was self-serve. The product could have been self-serve with a better cohort filter. Marketing needed guardrails. Sales needed a recommendation engine, not a dashboard. Finance needed raw data with scenario modeling. We called them all "self-serve analytics users" and gave them all the same tool. That's a governance failure disguised as a product decision.
I rebuilt the dashboard. But the rebuild wasn't what you'd expect.
\ I didn't add more charts. I added fewer. I removed three tabs and consolidated the remaining one around a single question: "Is this metric healthy, concerning, or critical?" I added conditional formatting that turns cards red, yellow, or green based on thresholds the team defined. I'm not proud of how simple it looks now. It looks like something a first-year analyst would build. But it gets used.
\ For Product, I built a separate cohort comparison tool. It's ugly. It's a parameterized Looker Explore with two date pickers and a delta calculation. It does one thing.
\ For Marketing, I added a composite score that combines volume, retention, and contract value into a single channel effectiveness metric. They can still see the components, but the default view answers the actual question: which channel is best per dollar retained.
\ For Sales, I gave up on dashboards entirely. I built a scored account list that runs weekly, ranks accounts by upsell signals, and lands in a Slack channel. It took less time to build than the dashboard tab I replaced.
\ For Finance, I created a Google Sheet template that pulls live data via the Looker API. They can model on top of real numbers without exporting manually.
\ The common thread: I stopped asking "what metrics does this team need?" and started asking "what decision does this team make repeatedly, and what's the shortest path from data to that decision?"
Build for the decision, not the data. If you can't name the specific decision a dashboard is supposed to support, you're building a museum exhibit. People will visit once, nod politely, and never come back.
\ Watch someone use your dashboard before you ship it. Not a stakeholder demo where they nod along. An actual work session where they try to answer a question they care about. You will learn more in twenty minutes of observation than in a month of requirements gathering.
\ The best BI isn't always a dashboard. Sometimes it's a Slack alert. Sometimes it's a spreadsheet with live data. Sometimes it's a scored list. The medium should match the decision pattern, not the other way around.
\ And if your usage logs show that people open your dashboard and leave within two minutes, the dashboard isn't slow. It's not answering their question.
\ The hardest part of business intelligence isn't building the data model. It's understanding what people actually do when they open your work.
2026-03-06 00:52:03
As many of you know, I'm always trying to share knowledge — whether through videos, talks, or interviews. And from every session, I like to extract the most powerful moments and turn them into Shorts.
But there’s a problem.
Most tools that can help me do this easily are paid. And they don't cost just a few bucks; they're quite expensive.
Now, I'm not being cheap. But I thought:
An engineer built this tool. I'm an engineer too. So I can build my own."
And then I reflected:
Well… not just me. **Me + Claude. \ And that's how *Video Wizard* was born — an open-source, AI-powered tool for turning long-form video into short-form content with subtitles, smart cropping, and professional templates.
In this post, I'll walk you through the architecture, the tech decisions, and what I learned building a production-grade video processing pipeline as a side project.
\n Here's the full user flow:
But it's not just a clip extractor. There's also a standalone Subtitle Generator that skips the AI analysis and goes straight from upload to rendered subtitles, as well as a Content Intelligence tool for analyzing transcripts without video. \n
I chose a microservices monorepo approach with Turborepo. Three independent services, each doing what it does best:
Why three services?
:::info Key Insight: Video as React Components
This was the "aha" moment for me. \n I chose Remotion because it lets you treat video like a UI. Components, props, composition — but applied to audiovisual content.
:::
The most interesting algorithmic challenge was the smart cropping. When you convert a 16:9 video to 9:16, you need to decide where to crop — and ideally, you follow the speaker's face.
\n The processing engine uses MediaPipe's BlazeFace model for detection, then applies aweighted scoring algorithmwhen multiple faces appear
\n The result? Cinematic-quality camera movement that tracks the speaker without the "security camera" feel. And it's smart enough to skip face detection entirely when the source video already matches the target aspect ratio. \n
Getting subtitles to sync properly across three services with different time formats was the trickiest part.
Stage: Whisper output \n Format: Seconds \n Example: { start: 0.5, end: 2.3 }
Stage: Frontend editor \n Format: Milliseconds \n Example: { start: 500, end: 2300 }
Stage: Remotion renderer \n Format: Seconds \n Example: { start: 0.5, end: 2.3 }
One early bug had 60-second videos rendering as 0.06 seconds because the times were getting divided by 1000 twice. Fun times.
I also added a configurable 200ms subtitle offset to account for the perceptual delay between hearing a word and reading it:
const SUBTITLEOFFSET = 0.2; // seconds \n const adjustedTime = currentTime - SUBTITLEOFFSET;
It’s a small detail, but it makes the subtitles feel perfectly synced.
Beyond basic editing, I built automated detection for common subtitle issues:
These are pure functions — no side effects, easily testable:
const result = detectIssues(subtitles, config); \n const cleaned = removeDetectedIssues(subtitles, result.issues);
With one click, subtitles go from raw Whisper output to clean, professional captions.
Screaming Architecture
The folder structure tells you what the app does before you read a single line of code:
features/video/components/ // Renders video UI
hooks/ // Manages video state
containers/ // Orchestrates video workflows
types/ // Defines video data shapes
lib/ // Provides video utilities
Strict Separation of Concerns
API routes are thin. They only handle HTTP and delegate to services:
export async function POST(request: NextRequest) {
const body = await request.json();
const data = await subtitleGenerationService.generateSubtitles(body);
return NextResponse.json({ success: true, data });
}
All business logic lives in service classes — reusable, testable, and independent of HTTP:
export class SubtitleGenerationService {
async generateSubtitles(input) { // 1. Call Python transcription // 2. Convert time formats // 3. Structure response }
async renderWithSubtitles(input) { // 1. Send job to Remotion // 2. Poll until complete // 3. Return video URL }
}
Every external boundary is validated with Zod. Types are inferred, not duplicated:
const BrandKitSchema = z.object({
logoUrl: z.string().optional(),
logoPosition: z.enum(['top-left', 'top-right', 'bottom-left', 'bottom-right']),
logoScale: z.number().min(0.1).max(2),
primaryColor: z.string().regex(/^#[0-9A-Fa-f]{6}$/).optional(),
});
type BrandKit = z.infer<typeof BrandKitSchema>;
Types come from schemas — not the other way around.
This project would have taken months working solo. With Claude as a pair programmer, I went from idea to working prototype significantly faster. Not because the AI wrote everything, but because it accelerated the tedious parts — boilerplate, FFmpeg flags, Remotion configuration — so I could focus on architecture and product decisions.
\
We increasingly depend on external SaaS for everything. Sometimes the best way to learn is to build the tool yourself. You’ll understand video processing, ML pipelines, and rendering engines at a depth that no tutorial can give you.
\
If you’re building anything with subtitles, pick one time format (seconds or milliseconds) and stick with it. Document your conversions. Test edge cases. Your future self will thank you.
This is still a personal project, but it already includes:
Roadmap ideas:
The repo is open source. You can run the entire stack locally
I’d love your feedback:
PRs, issues, and stars are all welcome.
GitHub: https://github.com/el-frontend/video-wizard
Built with Next.js, Python, Remotion, and a lot of help from Claude.
\
2026-03-06 00:34:57
Singapore, Singapore, March 5th, 2026/Chainwire/--iZUMi Finance has announced a strategic agreement with CIMG Inc. (Nasdaq: IMG) (“CIMG”), a Nasdaq-listed digital asset company, under which CIMG intends to pursue the proposed acquisition of selected key assets, core patents, and intellectual property from iZUMi Finance.
The proposed acquisition builds on the firms’ prior engagement, including the jointly launched $20 million Upstarts Fund, and represents a significant step in CIMG’s strategy to expand its institutional decentralized finance (DeFi) infrastructure.
Through the acquisition of iZUMi Finance’s technology assets and liquidity infrastructure, CIMG aims to strengthen its DeFi architecture and deepen its presence within on-chain liquidity markets.
Under the proposed acquisition framework, CIMG intends to incorporate iZUMi Finance’s multi-chain liquidity technologies, liquidity management mechanisms, and governance infrastructure into its digital asset architecture.
These acquired technologies are expected to enhance on-chain capital efficiency and support optimized treasury yield generation, particularly from Bitcoin held within CIMG’s treasury. As part of the broader acquisition structure, CIMG also plans to acquire $IZI tokens for long-term staking and governance participation within the iZUMi ecosystem.
The proposed acquisition is designed to strengthen CIMG’s DeFi infrastructure capabilities through the integration of iZUMi Finance’s intellectual property and liquidity technologies. By incorporating these assets into its institutional digital asset framework, CIMG aims to enhance on-chain liquidity management and improve capital efficiency across decentralized markets.
iZUMi Finance is a multi-chain DeFi protocol providing one-stop DEX-as-a-Service. Its flagship product, iZiSwap, is a leading multi-chain DEX built on the innovative DL-AMM (Discretized Liquidity AMM) design, and is the first concentrated liquidity DEX supporting on-chain Order Book features like CEX.
CEO of iZUMi Finance
Jimmy
:::tip This story was published as a press release by Chainwire under HackerNoon’s Business Blogging Program
:::
Disclaimer:
This article is for informational purposes only and does not constitute investment advice. Cryptocurrencies are speculative, complex, and involve high risks. This can mean high prices volatility and potential loss of your initial investment. You should consider your financial situation, investment purposes, and consult with a financial advisor before making any investment decisions. The HackerNoon editorial team has only verified the story for grammatical accuracy and does not endorse or guarantee the accuracy, reliability, or completeness of the information stated in this article. #DYOR
\
2026-03-06 00:20:11
This guide compares seven of the best free currency converter APIs developers can use in 2026 to integrate real-time foreign exchange data into applications. It explains how currency APIs work, what features to evaluate—like update frequency, historical data, and uptime—and highlights the strengths of popular options such as Fixer, Exchangerates API, Open Exchange Rates, Currencylayer, XE, Currency API, and IBAN. The article also includes example requests, use-case recommendations, and practical guidance to help developers choose the right API for fintech apps, e-commerce platforms, analytics dashboards, or early-stage MVPs.
2026-03-06 00:03:13
How are you, hacker?
🪐 What’s happening in tech today, March 5, 2026?
The HackerNoon Newsletter brings the HackerNoon homepage straight to your inbox. On this day, Homebrew Computer Club Holds First Meeting in 1975, Yahoo! Officially Launches in 1955, and we present you with these top quality stories. From The Ambies, Imperfectly: A Night of Good Intentions and Unfortunate Surprises to Nano’s Pitch: A Currency That Actually Works, let’s dive right in.
By @omotayojude [ 3 Min read ] Learn the technical secrets of how Apple Pay and Google Pay handle refunds through tokenization. Read More.
By @emmimalpalexander [ 9 Min read ] A reproducible study shows why removing activations makes deep nets collapse into linear models—plus gradient behavior, depth effects, and boundaries. Read More.
By @axsaucedo [ 19 Min read ] Learn how to monitor multi-agent AI systems with OpenTelemetry and SigNoz using KAOS on Kubernetes, tracing LLM calls, tool usage, and agent delegation. Read More.
By @anson [ 6 Min read ] Nano is one of the few cryptocurrencies with a real ability to make the work a better place, but its being held back due to economics. Read More.
By @recognized [ 9 Min read ] The 2026 Ambies arrived under pressure, a historic storm, delayed ceremony, and mounting questions about the Podcast Academys direction. Read More.
🧑💻 What happened in your world this week?
It's been said that writing can help consolidate technical knowledge, establish credibility, and contribute to emerging community standards. Feeling stuck? We got you covered ⬇️⬇️⬇️
ANSWER THESE GREATEST INTERVIEW QUESTIONS OF ALL TIME
We hope you enjoy this worth of free reading material. Feel free to forward this email to a nerdy friend who'll love you for it.See you on Planet Internet! With love, The HackerNoon Team ✌️
