--- Day changed Tue Sep 05 2017
marioxccHELLO05/09 17:14
joel135Is there a way to quickly add all missing cases in a definition?05/09 17:49
joel135oh, you can write myfun = ? and then ^C^L and ^C^C some times and it will only add the cases that are missing05/09 17:50
joel135good05/09 17:50
joel135Could I get some advice on this code? I am not very happy with the [_]... injections. It would be better if they were implicit somehow. But you can't define subtypes of inductive types, can you? It would be natural that all Countries be Nouns (or perhaps Things, but that's a linguistic matter).05/09 17:57
joel135https://pastebin.com/TEPbfqmf05/09 17:58
joel135It's a lot of fun to write the Translate module by the way. Pattern matching on grammar rules.05/09 18:02
kclancyjoel135: you might want to make Citizen and Language record types, if you expect to keep only one constructor. This will allow you to pattern match on values of these types in let bindings.05/09 21:09
kclancyjoel135: a bigger issue is that you want subtyping. Maybe it would be better then to disregard my previous advice, and instead make one big data type where each of the types you currently have are constructors.05/09 21:13
joel135Do you mean that each old type is a single constructor in the new type?05/09 21:16
kclancyjoel135: not all of them, actually just "bottom level" ones. Classifier types like Noun would be changed to proof types. n05/09 21:16
joel135That sounds flexible.05/09 21:17
joel135What does "proof type" mean in relation to this new type?05/09 21:18
kclancyJoel135: Noun would change to IsNoun, and it would be given an argument of type BottomLevel. IsNoun v would be the type of proofs that the Bottom level value v is a noun.05/09 21:20
kclancyThere would be one constructor for each way of proving something is a noun.05/09 21:21
joel135Is IsNoun defined inductively outside the big class?05/09 21:21
kclancyYes05/09 21:21
joel135Ok thanks a lot!05/09 21:21
joel135Do you think there will be any downsides to this method?05/09 21:21
kclancyNot sure, I'm kind of an Agda been.05/09 21:22
joel135Sorry, what does that mean?05/09 21:23
kclancyMy cell phone auto-correct changed newb to been.05/09 21:23
joel135oh alright05/09 21:24
kclancyBrb05/09 21:24
kclancyBasically, the approach I just proposed would require you to make heavy use of Agda's dependent types. Since you chose to use Agda in the first place, I assume dependent types are probably not something you are trying to avoid.05/09 21:26
joel135The more exposure to such things the better.05/09 21:27
kclancyI can type a sketch of some of the data definitions you would need in my approach. Just a sec.05/09 21:27
kclancyI'll post it on pastebin.05/09 21:27
joel135Ok05/09 21:27
kclancyjoel135: https://pastebin.com/NXA7giun05/09 21:39
joel135I hope (x : Object) can be made implicit in _,_어 : (x : Object) → (p : IsCountry x) → Object. I've left my computer for now. Time for some sleep!05/09 21:44
joel135And thanks again!05/09 21:46
kclancyYou're welcome05/09 21:46

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