Idris thread

>>8424859
Mhm, btw., what can one say about inverses of functions in dependent function types.

E.g. there may be
[math] f^{-1}:b\to a [/math]

But what about
[math] g^{-1}: ? \to a [/math]

>>8424871

Depends on P(a).
> literally.

>>8425334
Mhm, a little vague, but my call for an "inverse" surely was even more vague.

I also notice that my notation wasn't very good.
To make it consistent, if

[math] f : a \to b [/math]

then we should wrtie

[math] g : \prod_{x:a} b(x) [/math]

I now recognize that if we keep track of the argument for g via

[math] G : a \to \sum_{x:a} b(x) [/math]
[math] G(x) := (x, g(x)) [/math]

and

[math] \pi_1 : \sum_{x:a} b(x) \to a [/math]
[math] \pi_1 (x, y) := x [/math]

we get

[math] \pi_1 \circ G = id_a [/math]

In the other direction, just to specficy the domain, we must construct the type of elements that make up some section construction from g.

I'd like to try Idris, is it advisable to learn haskell first? Is it just haskell with constrained types?

>>8425596
No, Idris has dependent types. Dependent types are "better" than what standard Haskell offers (System Fc). Just jump straight in. There's no point in learning Haskell just to use Idris later.

>>8425596
The online tutorial/book will be introductory enough.
Difference is that Haskell has a much larger community and a far better compiler developed by a bunch of people and - the compiler does intelligent type inference and, given the type, may compute part of your code for you.
Idris is also just a starting point to see what "type driven developement", as the books title says, could bring to the table beyond Haskell. The latter is said to develop into the dependent direction in any case, btw.

File: 12083946_1012986602056231_682349838_n.jpg (31KB, 720x960px) Image search: [Google]

31KB, 720x960px

I like reading and ranting - the Idris book isn't freely available - does anybody have another suggestion they may find a broader participation?

File: Type-Theory-And-Formal-Proof-Nederpelt-Rob.jpg (16KB, 280x400px) Image search: [Google]

16KB, 280x400px

>>8428444
What about 'Type Theory and Formal Proof'? It ain't free but it's on libgen.

File: Rory_Ulysses.png (280KB, 500x376px) Image search: [Google]

280KB, 500x376px

>>8429688
Well na, I'm already disappointed with the participation at the Robotics thread - I'd try to organize people work something with many people interested. And you know, even if you discuss something basic - like analysis - advanced people can find interesting tangents too.

>>8430031
I think the participation is always going to be shit. I remember at least two reading groups on /sci/ and three on /lit/. All of them failed prematurely, even though some of them had a fairly wide attendance in the beginning.

File: 12067214_1012986558722902_2030323995_n-2.jpg (118KB, 720x960px) Image search: [Google]

118KB, 720x960px

>>8430055
I actually bought a copy of Infinite Meme.
How long do the summer reading groups last for it?

>>8430495
Are you literally riding a high horse?

File: IMG_2463.jpg (972KB, 3264x2448px) Image search: [Google]

972KB, 3264x2448px

>>8432540
Merlin is not made of cardboard, if that's your question

On board with Idris? Other ideas?