Deriving Dependently-Typed OOP from First Principles
The paper delves into the expression problem in programming, comparing extensibility in functional and object-oriented paradigms. It introduces dependently-typed object-oriented programming, emphasizing duality and showcasing transformations. Additional appendices are included for OOPSLA 2024.
Read original article
The paper discusses the expression problem in programming, highlighting the challenges of extending types with new producers and consumers simultaneously. It contrasts functional and object-oriented programs in terms of extensibility. The focus is on dependently-typed object-oriented programming, exploring it from first principles through duality. The authors derive a dependently typed calculus with dual language fragments, showcasing transformations like defunctionalization and refunctionalization. The paper emphasizes explaining dependently typed programming constructions as instances of duality. This extended version includes additional appendices not present in the published version, which will be part of the PACMPL issue for OOPSLA 2024. The work aims to fill a gap in the programming language landscape by systematically integrating dependent types into an object-oriented framework. The approach taken involves starting from a data-oriented language and deriving its dual fragment methodically. The implementation of this language and transformations serves to elucidate the relationship between functional and object-oriented paradigms in dependently typed programming.
Related
F (2006)
F is a functional concatenative language with K3 list operations and Joy's dip combinator. It enforces one-time assignment, supports floating-point and symbolic datatypes, and emphasizes function-valence and -charge theories. The language is purely functional, prohibiting side-effects and reassignment, with various primitives for arithmetic, logic, and list operations. F also provides interactive commands for debugging and manipulation, focusing on simplicity, efficiency, and functional programming paradigms.
As you learn Forth, it learns from you (1981)
The Forth programming language is highlighted for its unique features like extensibility, speed, and efficiency. Contrasted with Basic, Forth's threaded code system and data handling methods make it versatile.
Flambda2 Ep. 2: Loopifying Tail-Recursive Functions
Flambda2's Episode 2 explores Loopify, an optimization algorithm for tail-recursive functions in OCaml. It transforms recursion into loops, enhancing memory efficiency without compromising functional programming principles.
Memory Model: The Hard Bits
This chapter explores OCaml's memory model, emphasizing relaxed memory aspects, compiler optimizations, weakly consistent memory, and DRF-SC guarantee. It clarifies data races, memory classifications, and simplifies reasoning for programmers. Examples highlight data race scenarios and atomicity.
Optimizing the Roc parser/compiler with data-oriented design
The blog post explores optimizing a parser/compiler with data-oriented design (DoD), comparing Array of Structs and Struct of Arrays for improved performance through memory efficiency and cache utilization. Restructuring data in the Roc compiler showcases enhanced efficiency and performance gains.
7 comments> the essence of object-oriented programming is programming against interfaces, which correspond to the type theoretic concept of codata and copattern matching
They then use the classic codata example of a Stream, with a head and a tail. The Stream they declare looks a lot more like the version of that concept in functional languages than the version of it in an OO one, but clearly it exists in both paradigms.
https://www.cs.cmu.edu/~15150/resources/libraries/stream.pdf https://hackage.haskell.org/package/Stream-0.4.7.2/docs/Data... https://docs.oracle.com/en/java/javase/21/docs/api/java.base...
https://polarity-lang.github.io/oopsla24/#ChurchEncodingCoda...
Which makes me wonder what the next steps for a proof assistant based on this is. Will the de-/refunctionalization play an active role in the proof assistant as well, thus solving it as described in section 4.1?
Related
F (2006)
F is a functional concatenative language with K3 list operations and Joy's dip combinator. It enforces one-time assignment, supports floating-point and symbolic datatypes, and emphasizes function-valence and -charge theories. The language is purely functional, prohibiting side-effects and reassignment, with various primitives for arithmetic, logic, and list operations. F also provides interactive commands for debugging and manipulation, focusing on simplicity, efficiency, and functional programming paradigms.
As you learn Forth, it learns from you (1981)
The Forth programming language is highlighted for its unique features like extensibility, speed, and efficiency. Contrasted with Basic, Forth's threaded code system and data handling methods make it versatile.
Flambda2 Ep. 2: Loopifying Tail-Recursive Functions
Flambda2's Episode 2 explores Loopify, an optimization algorithm for tail-recursive functions in OCaml. It transforms recursion into loops, enhancing memory efficiency without compromising functional programming principles.
Memory Model: The Hard Bits
This chapter explores OCaml's memory model, emphasizing relaxed memory aspects, compiler optimizations, weakly consistent memory, and DRF-SC guarantee. It clarifies data races, memory classifications, and simplifies reasoning for programmers. Examples highlight data race scenarios and atomicity.
Optimizing the Roc parser/compiler with data-oriented design
The blog post explores optimizing a parser/compiler with data-oriented design (DoD), comparing Array of Structs and Struct of Arrays for improved performance through memory efficiency and cache utilization. Restructuring data in the Roc compiler showcases enhanced efficiency and performance gains.