Re: [TYPES] Book on Category Theory
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] My references are a little bit outdated but you can check: Basic category theory for computer scientists by Benjamin C. Pierce Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist by Andrea Asperti and Giuseppe Longo Cheers Beppe On 18/10/17 21:22, Aaron Gray wrote: [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] I am looking for a book on Category Theory that is ideally either aimed at Type Theory or has the relevant topics to support the area. I have bought three books on the topic so far, one 'Categories for Typesw' by Crole did not even cover covariance and contravariance.I would also like coverage of monoid and monads, and morphisms like anamorphisms and catamorphisms. I am also interested in papers applying category theory to areas of type theory. Suggestions of either online or printed material would be appreciated. Many tahnks in advance,
Re: [TYPES] I: On Dependent types and Subtyping's consistency
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] An older work in which you have a limited form of intersection types is: G. Castagna and G. Chen: Dependent types with subtyping and late-bound overloading. Information and Computation, vol. 168, n. 1, pag. 1-67, 2001. https://www.irif.fr/~gc/papers/infcomp99.pdf and you may be also interested in AC96b. D. Aspinall and A. Compagnoni. Subtyping dependent types. In Proc. 11th Annual Synposium on Logic in Computer Science, IEEE, pages 86–97, 1996 Beppe On 12/12/17 11:45, Gabriel Scherer wrote: [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] There is a language with dependent types and subtyping (including contravariant functions) in: Normalization by Evaluation for Sized Dependent Types Andreas Abel, Andrea Vezzosi, and Theo Winterhalter (2017) http://www.cse.chalmers.se/~abela/icfp17-long.pdf However, subtyping there is not "higher-order" in the sense of having type-indexed parameters themselves indicate a variance (you cannot abstract over all covariant parametrized types) -- pi-types only track relevant and irrelevant abstraction. In contrast, see the "higher-order subtyping" for F-omega-sub in Polarized Subtyping for Sized Types Andreas Abel, 2008 http://www.cse.chalmers.se/~abela/mscs06.pdf For higher-order subtyping in dependent systems, the two references I know of happen to be also mentioned on the nLab wiki: https://ncatlab.org/nlab/show/directed+homotopy+type+theory they are the work by Harper and Licata on directed type theory (and Dan Licata's PhD thesis), and Andreas Nuyts' master thesis. 2-Dimensional directed dependent type theory Robert Harper, Dan Licata, 2011 http://www.cs.cmu.edu/~drl/pubs/lh102dtt/lh102dtt.pdf Dependently Typed Programming with Domain-Specific Logics Dan Licata, 2011 http://www.cs.cmu.edu/~drl/pubs/thesis/thesis.pdf Towards a Directed Homotopy Type Theory based on 4 Kinds of Variance Andreas Nuyts, 2015 http://people.cs.kuleuven.be/~dominique.devriese/ThesisAndreasNuyts.pdf On Tue, Dec 12, 2017 at 10:57 AM, Giacomo Bergami
Re: [TYPES] Translation of bounded quantifications into intersection types
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 12/11/18 3:18 PM, Stephen Dolan wrote:
This suggests a different
definition of subtyping between polymorphic types: one polymorphic type is
a subtype of another if the first has more instances. Equivalently, one
polymorphic type is a subtype of another if for every instance of the
second, there is an instance of the first which is a subtype.
If you are interested in prenex polymorphism then let me point out the paper
"Set-theoretic Foundation of Parametric Polymorphism and Subtyping" in ICFP '11
(by Castagna & Xu) for a type system with union, intersection, and negation types.
There the subtyping relation is defined semantically: τ₁ ≤ τ₂ iff for all
possible interpretations of the type variables the first type is interpreted in
a subset of the second type. This in particular implies that for every type
substitution σ, τ₁ ≤ τ₂ implies τ₁σ ≤ τ₂σ
In this system not only you have
Bool → (α ∧ Real) ≤ Bool → (α ∧ Int)
but since you have "true" unions and intersections you can encode more general
bounded polymorphism of the form
∀ τ₁≤ α ≤ τ₂. τ
as
∀ α . τ'
where τ' is obtained from τ by replacing every occurrence of α by ((τ₁v α) ∧ τ₂)
The system also shows new applications of bounded polymorphism when combined
with negation types. For instance if you consider the function
fun x = if (x∈Int) then "ok" else x
then you want to give it the type
∀ α . (Int → String) ∧ (α\Int → α\Int)
that is, the type of a function that when applied to an integer it returns a
string and when applied to an argument of any type that is not an integer
returns a result of the same type (here / is the set-theoretic difference, i.e.
τ₁/τ₂ = τ₁ ∧ ¬τ₂). We can express this type in bounded polymorphism as
∀ α ≤ ¬Int. (Int → String) ∧ (α → α)
Notice that this type is not weird. It is exactly the type of the "balance"
function as defined by Okasaki for red-black trees in his book (you can find the
annotated code in section 3.3 of our POPL 15 paper "Polymorphic Functions with
Set-Theoretic Types: Part 2")
Finally, if you want to play with this kind of types, you can use the
development version of CDuce.
git clone https://gitlab.math.univ-paris-diderot.fr/cduce/cduce.git
use the cduce-next branch. In particular in the toplevel you can use two debug
directives:
> debug subtype τ₁ τ₂
that checks whether two types are in the subtyping relation and
> debug tallying [ ] [τ₁ , τ₂ ; ; τ₁' , τ₂']
that returns a set of solutions (type substitutions) for the set of constraints
{τ₁≤τ₂ ; ; τ₁'≤τ₂'}
(see #help debug for the syntax of debug directives and
http://www.cduce.org/manual_types_patterns.html#syntax for the syntax of types)
Re: [TYPES] type inference for mutually recursive algebraic types with subtyping
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
The work on extensible sum types (e.g. like the polymorphic variants of OCaml)
could be interesting for you if you don’t know about it already. A notable work
on this is “A polymorphic record calculus and its compilation” by Ohori (TOPLAS
1995), though it doesn’t discuss recursive types. A more recent one is
“Extensible programming with first-class cases” by Blume, Acar, and Chae (ICFP
2006).
These works, however, do not have true subtyping but use unification with a
notion of kinding for type variables (Ohori) or row variables (Blume et al.).
In our work at ICFP 2016 ("Set-theoretic types for polymorphic variants” by
Castagna, Petrucciani, and Nguyen) we have described type inference for a type
system with polymorphic variant types, union types, and recursive types, with
subtyping based on the “semantic subtyping” approach.
A revised version of that type inference system will be described in Tommaso
Petrucciani’s forthcoming PhD thesis (it is currently in the hands of the
reviewers, but I can send you a copy via PM if you wish). This is a major
revision of our ICFP paper. In particular the proof of completeness there was
not correct, and the thesis addresses this issue (by using techniques introduced
in Dolan's thesis already cited in previous messages) and provides a more robust
solution.
Cheers
Beppe
Re: [TYPES] subtyping of mutually recursive algebraic data types
[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ] In our ICFP 16 Paper /Set-Theoretic Types for Polymorphic Variants /we defined type inference for polymorphic variants with recursive set-theoretic types (type are defined coinductively with a couple of standard restrictions). https://urldefense.com/v3/__https://www.irif.fr/*gc/papers/icfp16.pdf__;fg!!IBzWLUs!QYIv5kZfRZ_sM_dbcvKdrXLsHb-tjd_4jpTeLE-n3m-E8TJ2qqx4c-2QqB1nepcRXZPlaUrqjL2yHCM5-OiV$ More generally, you may want to refer to Tommaso Petrucciani's PhD thesis /Polymorphic set-theoretic types for functional languages/ which studies type inference for recursive set-theoretic types (they can encode ADT' s via products and unions), which uses and improves some results of Stephen Dolan' s PhD thesis as well as of the paper cited above. https://urldefense.com/v3/__http://www.theses.fr/2019USPCC067__;!!IBzWLUs!QYIv5kZfRZ_sM_dbcvKdrXLsHb-tjd_4jpTeLE-n3m-E8TJ2qqx4c-2QqB1nepcRXZPlaUrqjL2yHFyPLk_c$ Hope it is useful Cheers Beppe On 17/06/2022 09.40, Aaron Gray wrote: [ The Types Forum,http://lists.seas.upenn.edu/mailman/listinfo/types-list ] I am interested if there is any work on the subtyping of mutually recursive algebraic data types. I am wanting an algorithm for purposes of implementing an object oriented programming language with ADT's which lower onto a virtual class implementation which can support mutually recursive behavior, but need the typ checking and inference at the ADT level. Theres a number of papers and projects in this area I have came across but none of them actually tackle algebraic data types properly let alone mutually recursive ones. A number inspired by Stephen Dolan's PhD Thesis and MLsub, his implementation. - Practical Subtyping for Curry-Style Languages by Rodolphe Lepigre and Christophe Raffalli - subml -https://urldefense.com/v3/__https://github.com/rlepigre/subml__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhSpE6cZJg$ - The Simple Essence of Algebraic Subtyping, Lionel Parreaux and simple-sub implementation -https://urldefense.com/v3/__https://github.com/LPTK/simple-sub__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhS4dNcEiw$ - A Mechanical Soundness Proof for Subtyping Over Recursive Types Timothy Jones David J. Pearce - https://urldefense.com/v3/__https://github.com/zmthy/recursive-types__;!!IBzWLUs!ROzY30gWHR0LPvTTZLo_Ep7ErCu0LhX2jrPKbFJ9uhVgSSx659leOfq_pNrPSAGgLExea89yhX9iVce14nA987dFVoNzXhRACugkxw$ None of these seem to deal with mutually recursive data types. I am interested in the papproach of using codata/coinduction and coalgebras and possibly bisimulation in order to deal with the mutually recursive nature of real world mutually recursive algebraic data types like for instance AST's of real world complex computer languages. Any projects, papers, thoughts, or implementations would be of interest. Regards, Aaron
