))
Aaron Stump talks about type theory, computational logic, and related topics in Computer Science on his short commute.
Are you ready to get computational superpowers? These are unique powers that will let you tackle all sorts of problems like a superhero! Join Maryanne in her wild adventures in LogicLand. It is a super secret place where only animals live; they are intelligent and witty -so naturally...laughter ensues! These stories will help kids develop complex problem-solving tools rooted-in computer science, and most importantly, help them learn computational thinking, a critical 21st-century skill, whic ...
I
Iowa Type Theory Commute
1
Intersections and Unions in Practice; Failure of Type Preservation with Unions
13:38
13:38
나중에 재생
나중에 재생
리스트
좋아요
좋아요
13:38
I discuss the perhaps surprising fact that union and intersection types are quite actively used and promoted for languages like TypeScript, also OO languages like Scala. I also try to explain briefly a counterexample to type preservation with union types, which you can find at the start of Section 2 of Barbanera and Dezani-Ciancaglini's paper "Inte…
I sketch the argument that pure lambda terms in normal form are typable using intersection types. This completes the argument started in the previous episode, that intersection types are complete for normalizing terms: normal forms are typable, and typing is preserved by beta-expansion. Hence any normalizing term is typable (since it reduces to a n…
Type systems usually have the type preservation property: if a typable term beta-reduces, then the resulting term is still typable. So typing is closed under beta-reduction. With intersection typing, typing is also closed under beta-expansion, which is a critical step in showing that intersection typing is complete for normalizing terms: any normal…
In a type system with intersection types, a term t that has type A and also has type B can be assigned the type 'A intersect B'. This episode begins Chapter 12 of the podcast on intersection types.저자 Aaron Stump
Responding to an email question from a listener, I explain how to derive a form of inconsistency from the assumption that True is related to False at type Bool.저자 Aaron Stump
I muse about the hopeless prospect of a single intrinsic conceptual decomposition of a problem domain in software engineering, and relate this to the idea of intrinsic identity we discussed recently for Relational Type Theory.저자 Aaron Stump
Where relational semantics for parametric polymorphism often includes a lemma called Identity Extension (discussed in Episode 10, on the paper "Types, Abstraction, and Parametric Polymorphism"), RelTT instead has a refinement of this called Identity Inclusion. Instead of saying that the interpretation of every closed type is the identity relation (…
I
Iowa Type Theory Commute
1
On the paper "The Girard-Reynolds Isomorphism" by Philip Wadler
10:52
10:52
나중에 재생
나중에 재생
리스트
좋아요
좋아요
10:52
I give a brief glimpse at Phil Wadler's important paper "The Girard-Reynolds Isomorphism", which is quite relevant for Relational Type Theory as it shows that relational semantics for the usual type for Church-encoded natural numbers implies induction. RelTT uses a generalization of these ideas to derive induction for any positive type family.…
I
Iowa Type Theory Commute
1
Equivalence of inductive and parametric naturals in RelTT
14:23
14:23
나중에 재생
나중에 재생
리스트
좋아요
좋아요
14:23
I talk through a proof I just completed that the type of relationally inductive naturals and the type of parametric naturals are equivalent. This is similar to proofs one can find in a paper of Philip Wadler's titled "The Girard-Reynolds Isomorphism", which I plan to discuss in the next episode.저자 Aaron Stump
I discuss how to define internalized relational typings, implicit products, and two forms of natural number types, in RelTT.저자 Aaron Stump
In this episode, I discuss the semantics of the proposed six type constructors of RelTT.저자 Aaron Stump
This episode begins Chapter 11 of the podcast, on Relational Type Theory. This is a new approach to type theory that I am developing. The idea is to design a type system based on the binary relational semantics for types, which we considered in Chapter 10. This episode recalls some of that semantics.…
This episode continues the introduction of RelTT by presenting the types of the language. Because the system is based on binary relational semantics, we can include binary relational operators like composition and converse as type constructs! Strange. The language also promotes terms to relations, by viewing them as functions and then taking their …
I
Iowa Type Theory Commute
1
On the paper "Types, Abstraction, and Parametric Polymorphism"
21:19
21:19
나중에 재생
나중에 재생
리스트
좋아요
좋아요
21:19
In this episode I discuss one of the greatest papers in the history of Programming Language's research, namely "Types, Abstraction, and Parametric Polymorphism" by the great John C. Reynolds. I summarize the two interconnected semantics for polymorphic types proposed by Reynolds: one which interprets types as sets and programs as members of those s…
I continue discussing the approach to HOAS from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page.저자 Aaron Stump
Today I discuss the construction of relational models of typed lambda calculus (say, System F), that support the idea of representation independence. This is a feature of a type theory where different implementations of the same interface can be proved equivalent, and used interchangeably in the theory. Only in the past couple years have researcher…
I start explaining an idea from my paper "A Weakly Initial Algebra for Higher-Order Abstract Syntax in Cedille", 2019, available from my web page. The goal is to encode a datatype (including its constructors, which we saw were troublesome for higher-order signatures generally in the previous episode) for application-free lambda terms, which I submi…
I discuss the problem of term models for higher-order signatures, following a prelude about the Edinburgh Logical Framework (LF) and higher-order datatypes.저자 Aaron Stump
I
Iowa Type Theory Commute
1
Lambda applicative structures and interpretations of lambda abstractions
10:13
10:13
나중에 재생
나중에 재생
리스트
좋아요
좋아요
10:13
Discussion of definitions in "Pre-logical relations" by Honsell and Sannella, particularly the notion of a lambda applicative structure (similar to a definition in John C. Mitchell's book "Foundations for Programming Languages'). In short, lambda abstractions get interpreted in combinatory algebras by compiling away the lambda abstractions in favor…
Also known as the Fundamental Property, this is a theorem stating that for every well-typed term t : T, and every logical relation R between algebraic structures A and B, the meaning of t in A is related by R to the meaning of t in B. I view it as a straightforward semantic soundness property, but where the semantics of types is this somewhat inter…
In this episode, I talk through a small (but intricate) example from a paper titled "Pre-logical relations" by Honsell and Sannella, showing that the set of logical relations is not closed under composition. That is, you can have a logical relation between structure A and structure B, and one between B and C, but the composition (while a relation) …
Logical relations are the relational generalization of the algebraic concept of a homomorphism -- but they go further in extending the notion of structure-preservation to higher-order structures. We discuss the basic definition in this episode.저자 Aaron Stump
Start of Chapter 10, on logical relations and parametricity. Basic idea of logical relation as the relational generalization of the algebraic idea of homomorphism. This is also the start of Season 2, as the fall academic year is just beginning here in Iowa.저자 Aaron Stump
The simplified version of Lamping's algorithm for optimal beta-reduction is discussed. We have duplicators which eat their way through lambda graphs. When copying a lambda abstraction, we send one duplicator down the variable port, and another down the body port. When they meet, they cancel each other and the duplication is done. But duplication ca…
I discuss some examples posted on my blog, QA9, which show that executables produced by ghc (the main implementation of Haskell) can exhibit non-optimal beta-reduction. Thanks to Victor Maia for major help with these.저자 Aaron Stump
I
Iowa Type Theory Commute
1
Lambda graphs with duplicators and start of Lamping's abstract algorithm
22:22
22:22
나중에 재생
나중에 재생
리스트
좋아요
좋아요
22:22
In this episode I talk about how to represent lambda terms as graphs with duplicator nodes for splitting edges corresponding to bound variables. I also start discussing the beginning of Lampings' abstract algorithm for optimal beta-reduction, in particular how we need to push duplicators inside lambda abstractions to initiate a lazy duplication.…
I
Iowa Type Theory Commute
1
Duplicating redexes as the central problem of optimal reduction
16:06
16:06
나중에 재생
나중에 재생
리스트
좋아요
좋아요
16:06
We discussed last time how with a graph-sharing implementation of untyped lambda calculus, it can happen that you are forced to break sharing and copy a lambda abstraction. We discuss in this episode the central issue with doing that, namely copying redexes and copying applications which could turn into redexes following other beta reductions. The …
Some background on optimal beta reduction: Levy, Lamping. The main problem to overcome is duplicating a lambda abstraction that is used in two different places in your term. The solution is to try to duplicate it incrementally.저자 Aaron Stump
Many termination checkers support lexicographic (structural) recursion. The lexicographic combination of orderings on sets A and B is an ordering on A x B where a pair decreases if the A component does (and then the B component can increase unboundedly) or else the A component stays the same and the B component decreases. Connections with nested re…
Well-founded recursion is a technique to turn recursion which decreases along a well-founded ordering into a structural recursion.저자 Aaron Stump
Another type-based approach to termination-checking for recursive functions over inductive datatypes is to use so-called Mendler-style iteration. On this approach, we write recursive functions by coding against a certain interface that features an abstract type R, which abstracts the datatype over which we are recursing; and a function from R to th…
Discussion of a compositional method of termination checking using so-called sized types. Datatypes are indexed by sizes, and recursive calls can only be made on data of strictly smaller size than the data as input to the recursion. Since the method is type-based, it is compositional: we can break out helper functions from a recursive function and …
I
Iowa Type Theory Commute
1
Noncompositionality of syntactic structural-recursion checks
13:03
13:03
나중에 재생
나중에 재생
리스트
좋아요
좋아요
13:03
Review of need for termination analysis for recursive functions on inductive datatypes. Discussion of a serious problem with syntactic termination checks, namely noncompositionality. A function may pass the syntactic termination check, but abstracting part of it out into a helper function may result in code which no longer passes the check. So we n…
Start of Chapter 8 of the podcast, on termination checking in type theory, and strong functional programming. Discussion of a little history of adding datatypes to the original pure type theory of Coq (called the Calculus of Constructions). Considering the most basic form of termination checking, which is checking syntactically that recursive calls…
Discussion of the basic idea of the Tait--Martin-Loef proof of confluence for untyped lambda calculus. Let me know any requests for what to discuss in Chapter 8!저자 Aaron Stump
Start of discussion on how to prove confluence for untyped lambda calculus. Also some discussion about the research community interested in confluence.저자 Aaron Stump
The basic property of confluence of a nondeterministic reduction semantics: if from starting term t you can reach t1 and also t2 (by two finite reduction sequences), then there is some t3 to which t1 and t2 both reduce in a finite number of steps. The use of confluence for ensuring completeness of the conversion-checking algorithm that tests conver…
Discussion of the connection between normalization and logical consistency. One approach is to prove normalization and type preservation, to show (in proof-theoretic terms) that all detours can be eliminated from proofs (this is normalization) and that the resulting proof still proves the same theorem (this is type preservation). I mention an alter…
I
Iowa Type Theory Commute
1
Normalization in type theory: where it is needed, and where not
16:28
16:28
나중에 재생
나중에 재생
리스트
좋아요
좋아요
16:28
Normalization (every term reaches a normal form via some reduction sequence) is needed essentially in type theory due to the Curry-Howard isomorphism: diverging programs become unsound proofs. Traditionally, type theorists have also desired normalization or even termination (every term reaches a normal form no matter what reduction sequence is expl…
Discussion of normalization (there is some way to reach a normal form) versus termination (no matter how you execute the term you reach a normal form). A little more discussion of strong FP. For type theory, the need for normalization due to Curry-Howard and due to conversion checking.저자 Aaron Stump
I
Iowa Type Theory Commute
1
Proving type safety; upcoming metatheoretic properties
13:07
13:07
나중에 재생
나중에 재생
리스트
좋아요
좋아요
13:07
Type safety proofs are big confirmations requiring consideration of all your operational and typing rules. So they rarely contain much deep insight, but are needed to confirm your language's type system is correct. Looking ahead, this episode also talks about the different between normalization and termination when your language is nondeterministic…
I
Iowa Type Theory Commute
1
The progress property and the problem of axioms in type theory
10:13
10:13
나중에 재생
나중에 재생
리스트
좋아요
좋아요
10:13
We review the metatheoretic property of type safety, decomposed into two properties called type preservation and progress. Discussion of progress in the context of type theory, where adding axioms can lead to a failure of progress.저자 Aaron Stump
Type safety is a basic property of both statically typed programming languages and type theories. It has traditionally (past few decades) been decomposed into type preservation and progress. Type preservation says that if a program expression e has some type T, then running e a bit will give a result that still has type T (and type preservation wou…
Metatheory is concerned with proving properties about theories, in this case type theories or programming languages.저자 Aaron Stump
We consider using Mendler's technique of abstracting out problematic types with new type variables, and how this can yield a lambda encoding where the programmer is in charge of when to make recursive calls (rather than in the Church encoding, where the data present the programmer's combining function with the results of all possible recursive call…
I
Iowa Type Theory Commute
1
The Mendler encoding and the problem of explicit recursion
10:59
10:59
나중에 재생
나중에 재생
리스트
좋아요
좋아요
10:59
The Church encoding allows definition of certain recursive functions, but all the recursive calls are implicit. The encoding simply presents you with the results of recursion for all immediate subdata. Using a technique due to Mendler, an encoding is possible where recursions are explicitly made by the combining functions given to the data.…
In this episode we briefly review the Church and Parigot encodings (discussed previously in Chapter 6 of this podcast) and then consider the Scott encoding, where combining functions receive only the immediate subdata of the data.저자 Aaron Stump
The Parigot encoding has exponential-size normal forms: but don't panic! With a decent graph-sharing implementation of lambda calculus, they take linear space in memory.저자 Aaron Stump
The Parigot encoding solves the Church encoding's problem of inefficient predecessor. It can be typed using positive-recursive types, which preserve normalization of the type theory.저자 Aaron Stump
What is fold-right for a natural number? How do we define addition with this? The problem of inefficient predecessor.저자 Aaron Stump
