--- Day changed Mon Mar 13 2017 | ||

quchen | What’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 |
---|---|---|

quchen | Is 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 foo | 13/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 equal | 13/03 09:21 |

{AS} | which is not necessarily true for all values of P x | 13/03 09:21 |

Eduard_Munteanu | quchen, values are more like type synonyms in Haskell | 13/03 09:28 |

Eduard_Munteanu | e.g. String : Set; String = List Char | 13/03 09:30 |

Eduard_Munteanu | Data declarations are more than just type functions, they give you constructors and eliminators. | 13/03 09:34 |

quchen | Eduard_Munteanu: Hmm. | 13/03 09:44 |

quchen | But what’s the difference between »Real -> Real -> Bool« and »Real -> Real -> Set«? | 13/03 09:45 |

quchen | There is an exercise asking to (try to) implement the two, where apparently the Bool version does not work. | 13/03 09:45 |

quchen | But 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_Munteanu | Neither 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 |

quchen | What’s Dec? | 13/03 09:48 |

quchen | Ah, it’s P a -> Dec a | \neg (P a) -> Dec a | 13/03 09:49 |

quchen | Or something along these lines | 13/03 09:49 |

Eduard_Munteanu | Yeah. | 13/03 09:49 |

Eduard_Munteanu | One Real -> Real -> Bool is the ordinary comparison for equality, whereas Real -> Real -> Set can return bottom or top depending on whether they're equal | 13/03 09:51 |

quchen | Eduard_Munteanu: Those seem pretty similar to me. | 13/03 09:51 |

quchen | Bools can be lifted to Set trivially, so the first implies the second. | 13/03 09:51 |

quchen | The other way round, oh I see, doesn’t work. | 13/03 09:51 |

quchen | isInhabited : Set → Bool :-) | 13/03 09:51 |

Eduard_Munteanu | Yeah, but it can lie. | 13/03 09:52 |

Eduard_Munteanu | (it has to) | 13/03 09:52 |

quchen | Still, 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 |

quchen | At some point I have to decide whether to be ⊥ or \top, no? | 13/03 09:53 |

Eduard_Munteanu | Well, there are many more inhabitants in Set. | 13/03 09:53 |

quchen | Hmmm. So you could just map two reals onto a type that is inhabited iff all reals support equality, for example? | 13/03 09:54 |

quchen | Oh and by the way, how do I input the questionmark-equals from the Agda standard lib? | 13/03 09:54 |

Eduard_Munteanu | \?==, IIRC | 13/03 09:55 |

quchen | _≟_ : Decidable {A = ℕ} _≡_ | 13/03 09:55 |

quchen | \?== huh okay | 13/03 09:55 |

canndrew | is there a way to make agda use multiple cpu cores when typechecking? | 13/03 11:42 |

gallais | canndrew: i guess that adding support for parallelism would entail a huge rewrite of the system | 13/03 12:10 |

gallais | such 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 |

canndrew | gallais: 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!