/home/laney/.irssi/irclogs/Freenode/#agda.log-20170314

--- Day changed Mon Mar 13 2017
quchenWhat’s the difference between a value and a data declaration? For example, take a value of the type »(a : xxx) -> Set« and a definition »data Foo (a : xxx) : Set where foo : Foo a«?13/03 09:10
quchenIs there a difference between the two so that I *have* to have an own data type for certain scenarios, and an ordinary function wouldn’t do?13/03 09:11
{AS}quchen: If you have P : a -> Set and a value px : P x you can't pattern match on px 13/03 09:20
{AS}whereas you can pattern match on foo13/03 09:21
{AS}Foo x *13/03 09:21
{AS}something you e.g. can prove is that all values of Foo x are equal13/03 09:21
{AS}which is not necessarily true for all values of P x13/03 09:21
Eduard_Munteanuquchen, values are more like type synonyms in Haskell13/03 09:28
Eduard_Munteanue.g. String : Set; String = List Char13/03 09:30
Eduard_MunteanuData declarations are more than just type functions, they give you constructors and eliminators.13/03 09:34
quchenEduard_Munteanu: Hmm.13/03 09:44
quchenBut what’s the difference between »Real -> Real -> Bool« and »Real -> Real -> Set«?13/03 09:45
quchenThere is an exercise asking to (try to) implement the two, where apparently the Bool version does not work.13/03 09:45
quchenBut isn’t showing that two reals are boolean-equal the same as showing that the Set is inhabited (or not)?13/03 09:46
Eduard_MunteanuNeither carry information about the reals equality.13/03 09:47
Eduard_Munteanu(x : Real) -> (y : Real) -> Dec (x == y)   on the other hand does.13/03 09:48
quchenWhat’s Dec?13/03 09:48
quchenAh, it’s   P a -> Dec a   |   \neg (P a) -> Dec a13/03 09:49
quchenOr something along these lines13/03 09:49
Eduard_MunteanuYeah.13/03 09:49
Eduard_MunteanuOne Real -> Real -> Bool is the ordinary comparison for equality, whereas Real -> Real -> Set can return bottom or top depending on whether they're equal13/03 09:51
quchenEduard_Munteanu: Those seem pretty similar to me.13/03 09:51
quchenBools can be lifted to Set trivially, so the first implies the second.13/03 09:51
quchenThe other way round, oh I see, doesn’t work.13/03 09:51
quchenisInhabited : Set → Bool :-)13/03 09:51
Eduard_MunteanuYeah, but it can lie.13/03 09:52
Eduard_Munteanu(it has to)13/03 09:52
quchenStill, I don’t see how I could write a function of type Real -> Real -> Set which would not also allow me to write a function Set -> Set -> Bool.13/03 09:53
quchenAt some point I have to decide whether to be ⊥ or \top, no?13/03 09:53
Eduard_MunteanuWell, there are many more inhabitants in Set.13/03 09:53
quchenHmmm. So you could just map two reals onto a type that is inhabited iff all reals support equality, for example?13/03 09:54
quchenOh and by the way, how do I input the questionmark-equals from the Agda standard lib?13/03 09:54
Eduard_Munteanu\?==, IIRC13/03 09:55
quchen_≟_ : Decidable {A = ℕ} _≡_13/03 09:55
quchen\?== huh okay13/03 09:55
canndrewis there a way to make agda use multiple cpu cores when typechecking?13/03 11:42
gallaiscanndrew: i guess that adding support for parallelism would entail a huge rewrite of the system13/03 12:10
gallaissuch a thing has been done recently for Coq and it comes with some caveats: (https://coq.inria.fr/refman/Reference-Manual031.html)13/03 12:11
canndrewgallais: damn, guess I need to find other ways to speed it up then :/13/03 12:16

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