Continue contributing to Idris via low-hanging fruit.
Get involved in Software Foundations in Idris.
type-class related QA for Haskell/Scala folk.
execute with alias exec when --execute and --exec are semantically different command line options.IRTS/Lang.hs about using LAlt' for all the IRs.idris-codegen-c.Equiv.v, assign_aequiv.[ ] Demystify predicative/impredicative.
[ ] Demystify intensional/extensional.
[ ] Demystify relational parametricity.
[ ] Demystify “logical relations”. aka apparently: “Tait’s method”, “the method of computability”, “realizability”, “Tait’s computability method” (PiMLTT).
[ ] β law (aka beta law). Seen on http://cstheory.stackexchange.com.
[ ] η law (aka eta law). Seen on http://cstheory.stackexchange.com.
[ ] Subject reduction
[ ] Reduction termination
[ ] “Church-Rosser property”. Seen in PiMLTT.
[ ] “convertability”. Seen in PiMLTT: “equality is convertibility in the sense of combinatory logic”.
[ ] “combinatory logic”. Seen in PiMLTT.
[ ] “convertability relation”. Seen in PiMLTT.
[ ] “ξ conversion is abandoned” (aka Xi conversion), PiMLTT.
[ ] Demystify “parametricity”.
[ ] Demystify “first-class polymorphism”.
[ ] Demystify “second-class polymorphism”.
[ ] Demystify “polymorphic recursion”.
[ ] Demystify “universal polymorphism”.
[ ] Demystify “relevance” — something to do with the distinction between TTs that separate Π and ∀ and those that don’t.
[ ] Demystify “existential polymorphism”.
See Andreas Rossberg’s comment(s) on Lambda the Ultimate.
It’s second-class vs first-class that matters
That’s not quite right. You seem to be assuming that you can always statically monomorphise universal polymorphism, but that is only true if polymorphism is second-class (*). And in that case, it is just as true for existential polymorphism (e.g., some SML compilers “monomorphise” modules routinely). As soon as you have first-class polymorphism, though (e.g., higher-ranked polymorphic types), you cannot do that anymore, neither for universal nor for existential polymorphism. Furthermore, as naasking pointed out, you can encode existentials with universals then, so there really is no difference in the degree of static knowledge. In short, the compile time vs run time distinction does not hinge on universal vs existential polymorphism, but on second-class vs first-class polymorphism (and existentials in Haskell happen to be first-class). (*) And in fact, not even then, as Haskell’s counter-example of polymorphic recursion shows – contrary to popular belief, type class polymorphism is not static in Haskell, not even in plain H’98. Common optimisations notwithstanding.
[ ] Encoding existentials with universals. See here.
[ ] “axiom of reducibility” (seen here)
Unfortunately, Girard found that this system [Martin-Löf first TT] contradictory, prompting Martin-Löf to adopt “Russel-style” predicative universes, severely limiting the expressiveness of the theory (by effectively removing the axiom of reducibility) and making it slightly more complex (but had the advantage of making it consistent).
[ ] “occurs-check” (seen here)
[ ] “congruence rules for equality” (seems like structural equality). Seen on OPLSS pi-forall videos.
[ ] “normal form (NF)” / “weak-head normal form (WHNF)”
CoC Calculus of Constructions
CoC
CoC is an intensional dependent type theory.CoC is Coqand’s PhD thesis which is naturally (but unfortunately) in French.CIC Calculus of Inductive Constructions
Adapted from https://github.com/type-theory/learn-tt
[ ] BabyIdris in Idris
trifecta and unbound (instead of parsec and unbound).2014 branch)master branch)Work on the real thing – contribute to Idris!
Everything is programming languages, isn’t it? However, leaving this heading to cover topics that don’t readily come under Type Theory etc.
Some references maybe not mentioned below:
bound
unbound
I am not a Number – I am a Free Variable by Conor McBride and James McKinna.
PHOAS
De Bruijn Indices
Locally Nameless
Abstract Binding Trees
Nominal Logic: A First Order Theory of Names and Binding
https://github.com/jyp/NameBindingSurvey/blob/master/WhiteBoard.md
http://requestforlogic.blogspot.com.au/2010/11/totally-nameless-representation.html
Namely Painless
HOS
Syntax for Free: Representing Syntax with Binding Using Parametricity Robert Atkey
Totally Nameless
http://research.microsoft.com/en-us/um/people/simonpj/Papers/inlining/ (Mentioned in Kmett’s bound tutorial)
Beluga seems to be a PL with built in support for name binding (contexts).
A Dependent Type Theory with Names and Binding A categorically yikes abstract.
We consider the problem of providing formal support for working with abstract syntax involving variable binders. Gabbay and Pitts have shown in their work on Fraenkel-Mostowski (FM) set theory how to address this through first-class names: in this paper we present a dependent type theory for programming and reasoning with such names. Our development is based on a categorical axiomatisation of names, with freshness as its central notion. An associated adjunction captures constructions known from FM theory: the freshness quantifier N, name-binding, and unique choice of fresh names. The Schanuel topos – the category underlying FM set theory – is an instance of this axiomatisation. Working from the categorical structure, we define a dependent type theory which it models. This uses bunches to integrate the monoidal structure corresponding to freshness, from which we define novel multiplicative dependent products Π∗ and sums Σ∗, as well as a propositions-as-types generalisation H of the freshness quantifier.
Collections of binding techniques:
Teach Yourself Logic: A Study Guide Peter Smith.
Are there other interesting part of Mathematical Logic other than Proof Theory? Wikipedia mentions the following sub fields:
[ ] Reinventing formal logic (article)
[ ] The Logic Notes, John Slaney, ANU
[ ] Constructive Logic (course), Thierry Coquand
Frank Pfennings Computation and Deduction Course and notes
[ ] How to Prove It, Velleman.
Practical Foundations of Mathematics, Paul Taylor.
for Heyting algebras
HoTT book
jonsterling: Conor’s insight is that you can define the graph of such a function as a well founded tree, and then compute by structural recursion on that tree
Agda/Coq/Cayenne
Can dependent records do (like in Cayenne)?
Agda seems to have a simple module system. See these slides.
You don’t need a fancy module system … and you tell me why I’m wrong.
generics-sop in Haskell these days. Introduction at https://github.com/kosmikus/SSGEP.any :: (a -> Bool) -> [a] -> Bool
any p = or . map p
Three Implementation Models for Scheme R. Kent Dybvig
Introduction to Scheme and it’s implementation
“Threaded code” interpreters
Cheney on the M.T.A.
ParentheC https://www.cs.indiana.edu/cgi-pub/c311/lib/exe/fetch.php?media=parenthec.pdf
Lambda, the Ultimate Label
Build Your Own Lisp (no GC)
90-mins-scc i.e. 90 minutes Scheme to C compiler
Other Lispy/Schemey implementations:
[VFPiA] Verified Functional Programming in Agda, Aaron Stump
The book is intended as an introduction for undergraduates who do not have a background in Agda, or type theory, or even functional programming. (Note that the book is not intended to be a reference on advanced features of Agda; that would be a great book for others on this list to write!) The goal of VFPiA is an introduction, for beginners, to ideas in applied type theory using Agda.
AKA “Package Management”
Nix is cool.