Good summer, well-formed people,
I was pointed into the direction of this book (1) and thought I'll open a thread on all things related. It looks pretty comprehensive and clear, and the first edition from 2012 is actually downloadable.
Besides, I'm considering delving into Idris (3) in the upcoming months and the main developer is publishing a book this summer as well (4).
(1)
https://ncatlab.org/nlab/show/Practical%20Foundations%20for%20Programming%20Languages
(2)
http://www.cs.cmu.edu/~rwh/plbook/book.pdf
(3)
http://docs.idris-lang.org/en/latest/tutorial/index.html
(4)
https://www.manning.com/books/type-driven-development-with-idris
>>8008449
Cool blog :^)
>>8008457
I could also ask a question, but I doubt anyone could really help me yet, and I don't want to bother the irc people too much. But here it goes:
Haskell already has exponential objects (a->b), and in fact the object map can even be used as function (->) in Haskell. In pic related, ":t" and ":k" is the quiery for the type or kind. "*" is basic kind, or, if you want, the category Hask of Haskell types, I've actually started to write down the semantics of it in (1).
Now Idris has dependent types and so I can define type formers where pass arrows f,g. I'm atm. triyng define Pullbacks, but I can't really into the syntax. What I got this far is
data Pullback : (f : x -> z) -> (g : y -> z) -> Type
where MkPullback : x -> y -> (f x = g y) -> Pullback f g
The point is that if you got exponential objects, pullbacks and truth values ({0,1} here), you should afaik already have everything you need for a topos.
Now [math] \times [/math] would be the pullback where z is a singleton.
data Singleton = Point
toPoint : Nat -> Singleton
toPoint n = Point
and now I'd like to define the term [math] (5,7) : {\mathbb N} \times {\mathbb N} [/math] in terms of Pullback. Help?
(1)
https://ncatlab.org/nlab/show/Haskell
>>8008507
Oh, and
\u => f
is
[math]\lambda u.\, f[/math]
in Idris.
In Haskell you have the function
(->)
so that
(->) a b
or
a->b
is
[math]hom(a,b)[/math],
while in Idris you have to write
\a,b => a->b
or
[math]\lambda a.\, \lambda b.\, hom(a,b)[/math]
because they use a->b also for dependent types [math] \prod_{u:a} b(u) [/math], i.e. the composition of -> isn't so simple in general. And the lambdas make use b can't depend on a.
who is this semen demon ?
Centipede mathematics is where you take a mathematical concept and see how many parts you can strip away without completely destroying its ability to function properly. For example, you can start with the concept of abelian group and try removing some things:
remove commutativity to get groups;
then remove inverses to get monoids;
or remove associativity instead of inverses to get loops;
etc (see group for more).
What still works? Abelian groups form an abelian category, while groups only form a semi-abelian category, so cohomology gets more complicated but still makes sense. Monoid representations (say on vector spaces) make as much sense as group representations, but loop representations are not apparently meaningful. Describing homomorphisms and presentations of monoids takes a little more care than for groups, while the naïve definitions continue to work for loops. Sometimes things actually work better; group objects make sense only in a cartesian monoidal category, while monoid objects make sense in any monoidal category. By seeing what are the salient features for making sense of things like cohomology and representation theory, we also see that we can generalise these, not by simply removing clauses from the definition of group, but by reworking the concept into such things as categories or quantum groups.
In the context of foundations, this is often called reverse mathematics. Here we remove axioms from set theory and consider what theorems can still be proved, which can be proved if reformulated into classically equivalent forms, and which are lost entirely (ideally provably so). On the Lab, some of us like to do this for constructive mathematics, but it is also important for internalization.
Certainly there is little value in proving isolated theorems like ‘Hemidemisemicontinous ‘Hemidemisemicontinuous functions are Leibniz-integrable.’ when one never really needs to integrate such general functions in such a restrictive way.
>>8008507
>The point is that if you got exponential objects, pullbacks and truth values ({0,1} here), you should afaik already have everything you need for a topos.
What do you mean when you say it [math]has[/math] truth values? Do you just mean it has a subobject classifier?
An elementary topos is defined as a category having a subobject classifier, being cartesian closed and having all finite limits. Having pullbacks implies it has all finite limits if you have a terminal object, which every cartesian closed category does.
It all comes down to what you mean when you say it has exponential objects - if you take "exponential object" to mean an object [math]X^Y[/math] satisfying the usual universal property mimicking function spaces, then this only implies the category is cartesian closed if you have a terminal object, which is what we needed to show that having pullbacks implied the existence of all finite limits.
So you need to add having a terminal object to your list to ensure it is a topos. I assume you do? I don't really know anything about this programming stuff, but that's the maths side of it.
>>8009361
Yes, the terminal objects are singletons {0} and the subobject classifier is !: {0}->{0,1}. It's all just like constructive set theory, so the only relevant question is if you can actually write down pullbacks.
Johan Georg Granström, Treatise on Intuitionistic Type Theory (2011).
>>8010632
http://bookzz.org/book/1133726/a3a0b0
Thx, looks like a well elaborated text. It's short, so I hope he makes his point while also giving a glimpse of other possible variants.
>>8010792
Okay I see the center of the book is mostly a long formal specification of his type theory.
The end is cute, in any case. I'm gonna post it to bump the thread.
lel bourbaki
>>8010818
do you use a software to make a picture of continuous pages?
>This page is to provide non-technical or maybe semi-technical discussion of the nature and role of the foundational system for mathematics known as homotopy type theory. For more technical details and further pointers see at homotopy type theory.
https://ncatlab.org/nlab/show/homotopy+type+theory+FAQ
>>8011154
I've done my bit to improve the Wikipedia article on HoTT, but the more I understand univalence, the less I have the feeling people are even close to produce anything practical and I hardly like anyone in the field (Bauer seems cool, no-homo, but Vladi is an ass and probably Steve Awodey too, and even if I strike up a chat with Mike Schulman, he responds flippant).
I like it from a philosophical perspective, though, I think. But I'm more on the practical side of math (although my friends would claim something else.) Btw. the guy who wrote the comprehensive intro book is also related to all things HoTT, from the CV page, but the book doesn't feature it.
>>8011136
>do you use a software
I could give an autistic answer to that, but let's not.
I just took the first screenshot and enlarged the canvas in photoshop so that the others fit in. It's quick. But I don't know what the guy above me did, who recommended the book posting the intro.
To what extent does equality in HoTT really mirror a notion of homotopical equality?
The definiton of equivalence at least seems more loose than the one in homotopy theory. The objects (they types that can be equated) seem more general.
>>8008449
Just wondering why you chose Idris instead of another dependently typed language like Agda or Lean?
>>8012239
I guess lean is far removed from Haskell (I really like the logo, in any case), and Haskell is the language with the good community.
Agda... I guess that relates to what I said above. If I look at the papers by the HoTT people, this is all going too slow and is too far removed from any application - I'm really interested in physicist and applications. Also, the use of ascii characters is idiosyncratic imho.
But that being said, I don't demand to use Idris in the future (they have more bugs too), it just seems the least autistic of the bunch.
buonp
does anybody understand lenses?
buoi
