--- Day changed Sat Jun 10 2017 | ||

Nik05 | thank you mietek | 10/06 01:14 |
---|---|---|

Nik05 | I expected to find a product in Data.Product but it looks more likes existential quantification. Where can I find the haskell product (,) or conjunction? | 10/06 01:16 |

Nik05 | And why can I only do a case distinction when I have one hole? | 10/06 01:32 |

Eduard_Munteanu | Nik05, a plain product is _×_. It is defined as a dependent sum, yes, A × B = Σ A (const B) | 10/06 04:55 |

mietek | "Nik05And why can I only do a case distinction when I have one hole?" | 10/06 11:43 |

mietek | Nik05: that’s not quite it | 10/06 11:43 |

mietek | Nik05: you can have multiple holes in different areas of the program | 10/06 11:43 |

mietek | Nik05: case splitting sometimes require you to have nothing on the right-hand side of the equation except a hole | 10/06 11:44 |

Nik05 | Thank you, Eduard_Munteanu | 10/06 11:53 |

Nik05 | oh hi mietek | 10/06 11:54 |

Nik05 | mietek I had a few times I had multiple holes on the rhs, so I could not case split. Needed to remove everything, case split, and put the same stuff back again | 10/06 11:54 |

mietek | Nik05: I recognise the situation, but I’m saying it’s not because of multiple holes | 10/06 11:56 |

Nik05 | Oké, but that is the error I get from agda | 10/06 11:57 |

mietek | what, Agda says "too many holes'? | 10/06 11:59 |

mietek | the same problem occurs if you have a single hole within a partial term on the RHS | 10/06 11:59 |

Nik05 | I think it Right hand side must be a single hole when making a case | 10/06 12:01 |

Nik05 | distinction | 10/06 12:01 |

Nik05 | -"I think it" | 10/06 12:01 |

mietek | right — I meant that you can have holes elsewhere in the program | 10/06 12:02 |

Nik05 | oh sorry | 10/06 12:02 |

Nik05 | Could you maybe explain how to use a pair in agda? × is just for types and (, ) for values? | 10/06 12:06 |

Nik05 | and what is the difference between ,’ and , ? When I look at the source ,’ is defined as , | 10/06 12:07 |

mietek | http://agda.github.io/agda-stdlib/Data.Product.html | 10/06 12:08 |

mietek | record Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where | 10/06 12:08 |

mietek | constructor _,_ | 10/06 12:08 |

mietek | first, understand this | 10/06 12:08 |

mietek | we define an Agda record type named Σ, that is parametrised by A and B | 10/06 12:09 |

mietek | Σ is known as a dependent pair | 10/06 12:09 |

mietek | because the second element of the pair may *depend* on the first element | 10/06 12:09 |

mietek | (a b are universe indices; ignore them for now) | 10/06 12:10 |

Nik05 | I expect that is for russels paradox | 10/06 12:11 |

mietek | yes | 10/06 12:11 |

mietek | elements of this type are constructed using _,_ | 10/06 12:11 |

mietek | now, a simple (non-dependent) pair is clearly also a dependent pair, where the second element ignores the first | 10/06 12:11 |

mietek | this it written in a convoluted fashion in the stdlib | 10/06 12:11 |

mietek | here’s a simpler way | 10/06 12:12 |

mietek | _×_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b) | 10/06 12:12 |

mietek | X × Y = Σ X (λ x → Y) | 10/06 12:12 |

Nik05 | Oké, that one I understand | 10/06 12:13 |

mietek | the distinction between types and values isn’t quite so clear in a dependently-typed language | 10/06 12:13 |

mietek | or rather, between types and terms | 10/06 12:13 |

mietek | so, to answer your question, look at the types :) | 10/06 12:14 |

mietek | _×_ wants two arguments that are Sets | 10/06 12:14 |

mietek | it will give a Set | 10/06 12:14 |

mietek | let’s call one such particular result P | 10/06 12:15 |

Nik05 | oké | 10/06 12:15 |

mietek | P = X × Y, for some particular X and Y | 10/06 12:15 |

mietek | _,_ can be used to construct elements of P, given an element of X, and an element of Y | 10/06 12:16 |

mietek | the type of _,_ is implied in the definition of the record | 10/06 12:17 |

Nik05 | x , (\ _ -> y) is than of type X × Y? | 10/06 12:18 |

mietek | myOwnComma : ∀ {a b} {A : Set a} {B : A → Set b} → (x : A) → B x → Σ A B | 10/06 12:18 |

mietek | myOwnComma = _,_ | 10/06 12:18 |

mietek | myOwnSimpleComma : ∀ {a b} {A : Set a} {B : Set b} → A → B → A × B | 10/06 12:18 |

mietek | myOwnSimpleComma = _,_ | 10/06 12:18 |

Nik05 | this I don't understand | 10/06 12:19 |

mietek | ok. what seems confusing? | 10/06 12:19 |

Nik05 | defining a function as another function, but being a different function | 10/06 12:20 |

mietek | would it be less confusing if I wrote "myOwnComma x y = x , y" ? | 10/06 12:20 |

mietek | that means the same thing | 10/06 12:21 |

Nik05 | but should that be "myOwnComma x y = x , (\_ -> y)" ? | 10/06 12:21 |

mietek | look again at the definition of Σ | 10/06 12:22 |

mietek | field | 10/06 12:22 |

mietek | proj₁ : A | 10/06 12:22 |

mietek | proj₂ : B proj₁ | 10/06 12:22 |

mietek | this is a confusing way of writing | 10/06 12:23 |

mietek | (x : A) → B x | 10/06 12:23 |

Nik05 | oh B proj1 | 10/06 12:23 |

mietek | B is a function from elements of A to Sets | 10/06 12:23 |

mietek | (to elements of Set b) | 10/06 12:23 |

mietek | in other words, B is not quite a type yet | 10/06 12:24 |

mietek | B needs a term to return a type | 10/06 12:24 |

mietek | hence, *dependent types* | 10/06 12:24 |

mietek | types that depend on terms | 10/06 12:24 |

Nik05 | I think I might get a grip on something | 10/06 12:24 |

mietek | good. understanding Σ is really fundamental. | 10/06 12:24 |

Nik05 | so Σ is a type depending on a Set and a type parameterised by that type | 10/06 12:25 |

Nik05 | and you can construct a value of type Σ by giving it an A and a (B A) | 10/06 12:26 |

mietek | Σ is a dependent pair, where the type of the second element of the pair depends on the value of the first element | 10/06 12:26 |

mietek | you can construct a value of type Σ by giving it an element of type A, named x, and also an element of type B x | 10/06 12:26 |

mietek | s/value/element/ | 10/06 12:27 |

Nik05 | oké | 10/06 12:27 |

mietek | yeah, human language isn’t so clear | 10/06 12:27 |

mietek | (the multiple meanings of "value" are in my head right now) | 10/06 12:27 |

Nik05 | I get the Σ type, but why define _,’_ ? | 10/06 12:28 |

Nik05 | It takes the same arguments and gives the same type? | 10/06 12:30 |

mietek | I’m not sure where that is | 10/06 12:31 |

mietek | oh, I see it | 10/06 12:31 |

mietek | it’s literally myOwnSimpleComma | 10/06 12:31 |

Nik05 | yes :P | 10/06 12:31 |

mietek | there’s no reason to do that except maybe have some simpler error messages | 10/06 12:31 |

Nik05 | oh oke | 10/06 12:31 |

mietek | in general, the stdlib isn’t a great model of code design | 10/06 12:32 |

mietek | (in my opinion) | 10/06 12:32 |

mietek | try defining your own things from scratch | 10/06 12:33 |

mietek | it’s a great learning exercise | 10/06 12:33 |

Nik05 | I was already doing that because I couldnt find a pair :P | 10/06 12:33 |

mietek | :) | 10/06 12:33 |

Nik05 | But when defining things myself do I need to include these Set levels? | 10/06 12:34 |

mietek | no | 10/06 12:34 |

mietek | not until you actually run into a universe level issue | 10/06 12:34 |

Nik05 | what is the difference between {a} (A : Set a) and (A : Set)? | 10/06 12:34 |

mietek | Set is Set₀ | 10/06 12:35 |

mietek | you can also use Set₁ etc | 10/06 12:35 |

mietek | Set₁ will get you out of most issues you will likely run into | 10/06 12:35 |

Nik05 | oke | 10/06 12:35 |

mietek | concretely | 10/06 12:36 |

mietek | https://mietek.github.io/imla2017/html/Semantics.html#1925 | 10/06 12:36 |

mietek | _⊨_ : Context → Type → Set₁ | 10/06 12:36 |

mietek | this has to be Set₁ because the definition quantifies over Model, which includes a Set | 10/06 12:36 |

mietek | that’s the only place in this particular work where I’ve had to go above level 0 | 10/06 12:37 |

mietek | oh yeah, and Model : Set₁ | 10/06 12:37 |

mietek | so that just propagates | 10/06 12:37 |

mietek | http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism | 10/06 12:39 |

Nik05 | Thank you very much mietek. I think I understand it a lot better now | 10/06 12:39 |

mietek | there is a lot of useful material in the old wiki | 10/06 12:39 |

mietek | you’re welcome | 10/06 12:39 |

Nik05 | I will bookmark it and read through it | 10/06 12:42 |

Nik05 | Thank you very much :) | 10/06 12:42 |

Nik05 | have a good afternoon | 10/06 12:42 |

Nik05 | I understand existential quantification alot better now | 10/06 14:15 |

mietek | :) | 10/06 14:15 |

mietek | constructive | 10/06 14:15 |

Nik05 | Are there other dependent types that are so fundamental? | 10/06 14:19 |

mietek | Π | 10/06 14:19 |

mietek | http://www.cs.bham.ac.uk/~mhe/AgdaTutorial/html/AgdaTutorial.html | 10/06 14:20 |

mietek | "The BHKCH intepretation of universal quantification" | 10/06 14:20 |

Nik05 | CH is Curry Howard? | 10/06 14:22 |

mietek | yes | 10/06 14:22 |

mietek | Π : ∀ {a b} → (A : Set a) (F : A → Set b) → Set (a ⊔ b) | 10/06 14:23 |

mietek | Π A F = ∀ (x : A) → F x | 10/06 14:23 |

mietek | in Agda, the built-in function arrow is Π | 10/06 14:23 |

mietek | it’s even more fundamental than Σ | 10/06 14:24 |

mietek | sorry, I misspoke | 10/06 14:26 |

mietek | "the built-in function arrow is Π" — that’s not exactly right | 10/06 14:27 |

Nik05 | oke | 10/06 14:27 |

mietek | but I don’t know how to explain this better | 10/06 14:27 |

mietek | gallais, Saizan; ^^ | 10/06 14:27 |

Nik05 | Thank you | 10/06 14:28 |

Nik05 | I will read into and ask about it when i got questions | 10/06 14:31 |

Nik05 | A proof of ∃ x ∈ S : φ ( x ) {\displaystyle \exists x\in S:\varphi (x)} \exists x\in S:\varphi (x) is a pair <a, b> where a is an element of S, and b is a proof of φ(a). | 10/06 16:14 |

Nik05 | this what i found about BHK on wiki | 10/06 16:15 |

Nik05 | so this pair is the dependent pair | 10/06 16:16 |

Nik05 | cool | 10/06 16:24 |

Nik05 | mietek what is the name of this pi sum/product? | 10/06 16:25 |

Nik05 | but how is this "builtin"? itsnt it just a function? | 10/06 16:40 |

mietek | Nik05: http://www.cse.chalmers.se/research/group/logic/book/book.pdf | 10/06 20:38 |

mietek | this is a bit overkill | 10/06 20:39 |

mietek | but… | 10/06 20:39 |

mietek | see page 11 | 10/06 20:39 |

Generated by irclog2html.py 2.7 by Marius Gedminas - find it at mg.pov.lt!