But I find such articles ridiculously hard to understand, especially system F (although I have been coding in #haskell for years).
Ironically, dependently-typed seem much simpler. In non-dependently-typed systems it's very hard to pinpoint the connections between types and terms. In dependently-typed systems, terms and types are the same thing.
"This talk is an invitation to embark on a journey to solve one of the most naive yet insanely convoluted open question in #software architecture: the problem of unit systems and physical quantities. As surprising as it may seem, in 2023, there is still no software library available in any of the most common programming languages that covers the issue in its full complexity including its myriad of edge cases. In the context of a standardization effort within the #cpp programming language committee #WG21 on the topic of units this talk constitutes an attempt to reach out to the #appliedcategorytheory community in order to approach the subject from a new angle.
Throughout the presentation, a particular attention will be put on the underlying reasons behind the emerging complexity of the subject and why applied category theory may be key to disentangle this apparent complexity. This will be illustrated by concrete applications in computational #physics and metrology, including particularly pathological cases that will put into question the very notion of what a unit is. Exploring conceptual boundaries through edge cases will help putting constraints on the mathematical structures that may be used to abstract the problem. Beyond the mere scope of being able to standardize a unit systems software library, the challenge raised in this talk represents a gateway to deep questions about physics, its language, its structure, and how to translate it into #typetheory. It also constitutes a perfect playground for applied category theory, going from a naive and well-framed question to an interdisciplinary open problem at the intersection of physics, computer science, and mathematics with broad impacts for programming languages and international standards."
If you are into programming languages, learning Ocaml (or other ML dialect like StandardML) makes a lot of sense, it's helpful for reading papers, watching conference talks, understanding basics of type theory, going through PL courses and all other fancy stuff.
Here is a good introductionary course on OCaml and functional programming:
has anyone written up an explanation of Yoneda in terms of logic? in particular it seems like a “metatheorem” about category theory with a similar kind of structure (and implications) to cut and identity admissibility as metatheorems about logics. is there anything there?
The Software Technology department at TU Delft is hiring new assistant and associate professors! This is an open call for any research field within one of our groups, so if you are a PL researcher and are interested to join us you are very welcome to apply. You can find more information about the positions and the application procedure at https://www.tudelft.nl/ewi/over-de-faculteit/afdelingen/software-technology/computer-science-open-call.
Getting interested in #Lean upon reading that the community isn't very concerned about whether it meets constructivists' criteria for theoretical soundness
Axiom K is an axiom in #TypeTheory, named due to the fact that if you use it too much you go into the "Axiom K-Hole" and your friends have to take care of you for the rest of the night.
"Something I'm curious about working on is an imperative dependently typed programming language that uses linear types and #TypeTheory to keep the mutation in line. Something I have to admit is that I'm not actually interested in #FunctionalProgramming. I'm simply interested in #types."
I have read 1 book( M. R. HOLMES, Elementary #SetTheory with a Universal Set -ISBN 2-87209-488-1)and one thesis ( #Constructivity and #Predicativity: Philosophical Foundations: crosella -2016) thoroughly . Among other things . Now I want to build up on these conceptual foundations, by pursuing this direction, could you suggest me , the relevent literature for this purpose? #typetheory#categoryttheory
if you start with a logic system and introduce a binary operator “:”, where “x: y” means “x is of type y,” alongside a few types, probably a universal type, probably a type type, a function type operator, etc., is that meaningfully inferior to many-sorted logic?
asking because i plan to prove some things in a system like this, and i’m wondering if i should figure out how many-sorted logic works instead. #logic #mathematicallogic #proof #typetheory
#introduction I've had this account since 2017, but I have to thank the Muskrat for pushing so many people over here, whom I'd like to keep following, for me to finally also spend some time here.
I'm hoping to see lots of discussions of homotopy type theory and related matters.