--- Day changed Sat Jun 10 2017
Nik05thank you mietek 10/06 01:14
Nik05I 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
Nik05And why can I only do a case distinction when I have one hole?10/06 01:32
Eduard_MunteanuNik05, 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
mietekNik05: that’s not quite it10/06 11:43
mietekNik05: you can have multiple holes in different areas of the program10/06 11:43
mietekNik05: case splitting sometimes require you to have nothing on the right-hand side of the equation except a hole10/06 11:44
Nik05Thank you, Eduard_Munteanu10/06 11:53
Nik05oh hi mietek 10/06 11:54
Nik05mietek 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 again10/06 11:54
mietekNik05: I recognise the situation, but I’m saying it’s not because of multiple holes10/06 11:56
Nik05Oké, but that is the error I get from agda10/06 11:57
mietekwhat, Agda says "too many holes'?10/06 11:59
mietekthe same problem occurs if you have a single hole within a partial term on the RHS10/06 11:59
Nik05I think it Right hand side must be a single hole when making a case10/06 12:01
Nik05distinction10/06 12:01
Nik05-"I think it" 10/06 12:01
mietekright — I meant that you can have holes elsewhere in the program10/06 12:02
Nik05oh sorry10/06 12:02
Nik05Could you maybe explain how to use a pair in agda? × is just for types and (, ) for values?10/06 12:06
Nik05and what is the difference between ,’ and , ? When I look at the source ,’ is defined as ,10/06 12:07
mietekhttp://agda.github.io/agda-stdlib/Data.Product.html10/06 12:08
mietekrecord Σ {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where10/06 12:08
mietek  constructor _,_10/06 12:08
mietekfirst, understand this10/06 12:08
mietekwe define an Agda record type named Σ, that is parametrised by A and B10/06 12:09
mietekΣ is known as a dependent pair10/06 12:09
mietekbecause the second element of the pair may *depend* on the first element10/06 12:09
mietek(a b are universe indices; ignore them for now)10/06 12:10
Nik05I expect that is for russels paradox10/06 12:11
mietekyes10/06 12:11
mietekelements of this type are constructed using _,_10/06 12:11
mieteknow, a simple (non-dependent) pair is clearly also a dependent pair, where the second element ignores the first10/06 12:11
mietekthis it written in a convoluted fashion in the stdlib10/06 12:11
mietekhere’s a simpler way10/06 12:12
mietek_×_ : ∀ {a b} → Set a → Set b → Set (a ⊔ b)10/06 12:12
mietekX × Y = Σ X (λ x → Y)10/06 12:12
Nik05Oké, that one I understand10/06 12:13
mietekthe distinction between types and values isn’t quite so clear in a dependently-typed language10/06 12:13
mietekor rather, between types and terms10/06 12:13
mietekso, to answer your question, look at the types :)10/06 12:14
mietek_×_ wants two arguments that are Sets10/06 12:14
mietekit will give a Set10/06 12:14
mieteklet’s call one such particular result P10/06 12:15
Nik05oké10/06 12:15
mietekP = X × Y, for some particular X and Y10/06 12:15
mietek_,_ can be used to construct elements of P, given an element of X, and an element of Y10/06 12:16
mietekthe type of _,_ is implied in the definition of the record10/06 12:17
Nik05x , (\ _ -> y) is than of type X × Y?10/06 12:18
mietekmyOwnComma : ∀ {a b} {A : Set a} {B : A → Set b} → (x : A) → B x → Σ A B10/06 12:18
mietekmyOwnComma = _,_10/06 12:18
mietekmyOwnSimpleComma : ∀ {a b} {A : Set a} {B : Set b} → A → B → A × B10/06 12:18
mietekmyOwnSimpleComma = _,_10/06 12:18
Nik05this I don't understand10/06 12:19
mietekok. what seems confusing?10/06 12:19
Nik05defining a function as another function, but being a different function10/06 12:20
mietekwould it be less confusing if I wrote "myOwnComma x y = x , y" ?10/06 12:20
mietekthat means the same thing10/06 12:21
Nik05but should that be "myOwnComma x y = x , (\_ -> y)" ?10/06 12:21
mieteklook again at the definition of Σ10/06 12:22
mietek  field10/06 12:22
mietek    proj₁ : A10/06 12:22
mietek    proj₂ : B proj₁10/06 12:22
mietekthis is a confusing way of writing10/06 12:23
mietek(x : A) → B x10/06 12:23
Nik05oh B proj110/06 12:23
mietekB is a function from elements of A to Sets10/06 12:23
mietek(to elements of Set b)10/06 12:23
mietekin other words, B is not quite a type yet10/06 12:24
mietekB needs a term to return a type10/06 12:24
mietekhence, *dependent types*10/06 12:24
mietektypes that depend on terms10/06 12:24
Nik05I think I might get a grip on something10/06 12:24
mietekgood. understanding Σ is really fundamental.10/06 12:24
Nik05so Σ is a type depending on a Set and a type parameterised by that type10/06 12:25
Nik05and 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 element10/06 12:26
mietekyou can construct a value of type Σ by giving it an element of type A, named x, and also an element of type B x10/06 12:26
mieteks/value/element/10/06 12:27
Nik05oké10/06 12:27
mietekyeah, human language isn’t so clear10/06 12:27
mietek(the multiple meanings of "value" are in my head right now)10/06 12:27
Nik05I get the Σ type, but why define _,’_ ?10/06 12:28
Nik05It takes the same arguments and gives the same type?10/06 12:30
mietekI’m not sure where that is10/06 12:31
mietekoh, I see it10/06 12:31
mietekit’s literally  myOwnSimpleComma10/06 12:31
Nik05yes :P10/06 12:31
mietekthere’s no reason to do that except maybe have some simpler error messages10/06 12:31
Nik05oh oke10/06 12:31
mietekin general, the stdlib isn’t a great model of code design10/06 12:32
mietek(in my opinion)10/06 12:32
mietektry defining your own things from scratch10/06 12:33
mietekit’s a great learning exercise10/06 12:33
Nik05I was already doing that because I couldnt find a pair :P10/06 12:33
mietek:)10/06 12:33
Nik05But when defining things myself do I need to include these Set levels?10/06 12:34
mietekno10/06 12:34
mieteknot until you actually run into a universe level issue10/06 12:34
Nik05what is the difference between {a} (A : Set a) and (A : Set)?10/06 12:34
mietekSet is Set₀10/06 12:35
mietekyou can also use Set₁ etc10/06 12:35
mietekSet₁ will get you out of most issues you will likely run into10/06 12:35
Nik05oke10/06 12:35
mietekconcretely10/06 12:36
mietekhttps://mietek.github.io/imla2017/html/Semantics.html#192510/06 12:36
mietek_⊨_ : Context → Type → Set₁10/06 12:36
mietekthis has to be Set₁ because the definition quantifies over Model, which includes a Set10/06 12:36
mietekthat’s the only place in this particular work where I’ve had to go above level 010/06 12:37
mietekoh yeah, and Model : Set₁10/06 12:37
mietekso that just propagates10/06 12:37
mietekhttp://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.UniversePolymorphism10/06 12:39
Nik05Thank you very much mietek. I think I understand it a lot better now10/06 12:39
mietekthere is a lot of useful material in the old wiki10/06 12:39
mietekyou’re welcome10/06 12:39
Nik05I will bookmark it and read through it10/06 12:42
Nik05Thank you very much :)10/06 12:42
Nik05have a good afternoon10/06 12:42
Nik05I understand existential quantification alot better now10/06 14:15
mietek:)10/06 14:15
mietekconstructive10/06 14:15
Nik05Are there other dependent types that are so fundamental?10/06 14:19
mietekΠ10/06 14:19
mietekhttp://www.cs.bham.ac.uk/~mhe/AgdaTutorial/html/AgdaTutorial.html10/06 14:20
mietek"The BHKCH intepretation of universal quantification"10/06 14:20
Nik05CH is Curry Howard?10/06 14:22
mietekyes10/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 x10/06 14:23
mietekin Agda, the built-in function arrow is Π10/06 14:23
mietekit’s even more fundamental than Σ10/06 14:24
mieteksorry, I misspoke10/06 14:26
mietek"the built-in function arrow is Π" — that’s not exactly right10/06 14:27
Nik05oke10/06 14:27
mietekbut I don’t know how to explain this better10/06 14:27
mietekgallais, Saizan; ^^10/06 14:27
Nik05Thank you10/06 14:28
Nik05I will read into and ask about it when i got questions10/06 14:31
Nik05A 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
Nik05this what i found about BHK on wiki10/06 16:15
Nik05so this pair is the dependent pair10/06 16:16
Nik05cool10/06 16:24
Nik05mietek what is the name of this pi sum/product?10/06 16:25
Nik05but how is this "builtin"? itsnt it just a function?10/06 16:40
mietekNik05: http://www.cse.chalmers.se/research/group/logic/book/book.pdf10/06 20:38
mietekthis is a bit overkill10/06 20:39
mietekbut…10/06 20:39
mieteksee page 1110/06 20:39

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