--- Day changed Mon Jul 17 2017
petercommandis it possible to model superclass dependencies like Num (A : Set) => Num (A -> A) with instance arguments in Agda?17/07 07:56
petercommandthe examples in http://agda.readthedocs.io/en/v2.5.2/language/record-types.html#id4 are non-recursive17/07 07:56
comietekpetercommand: look at the stdlib17/07 08:13
comietekpetercommand: especially the algebraic properties could be helpful17/07 08:13
comieteksemi group, group, etc17/07 08:13
comietekhttps://agda.github.io/agda-stdlib/Algebra.html17/07 08:14
petercommandcomietek: I am trying to have haskell-like typeclass in agda, why would the algebraic properties be helpful?17/07 08:16
petercommandam I missing something?17/07 08:21
comietekpetercommand: as examples17/07 08:21
petercommandthe examples in https://agda.github.io/agda-stdlib/Algebra.html don't have any use of instance arguments17/07 08:25
petercommand*don't use17/07 08:26
petercommand*don't use any17/07 08:26
petercommandwait, let me think about it17/07 08:27
petercommandcomietek: I think the examples in agda-stdlib/Algebra are more like the non-recursive versions17/07 08:36
comietekwhat exactly would you like to state?17/07 08:38
comietekI thought you had difficulty defining Num17/07 08:39
comietekbut perhaps I misunderstood17/07 08:39
petercommandum, no17/07 08:39
petercommandI want to pass Num (A -> A) as instance arguments implicitly17/07 08:39
comietekto what?17/07 08:40
comietekis there a function you're trying to define?17/07 08:40
petercommandlet me give an example17/07 08:40
petercommandhttps://pastebin.com/HVxNL28917/07 08:42
petercommandI want to pass toFuncNum implicitly to other functions17/07 08:42
petercommandsay, a function with signature forall (A : Set) -> Num (A -> A) -> ...17/07 08:43
petercommandI want the Num (A -> A) argument to be solved rather than given as an explicit argument17/07 08:43
petercommands/solved/infered17/07 08:44
comietekopen Num {{..}} public17/07 08:45
comietekinstance numForFunctions : {A : Set} {{_ : Num A}} -> Num (A -> A)17/07 08:45
comieteksomething like that17/07 08:45
comietekand then bind the implicit argument explicitly in the definition to use it17/07 08:46
comietekif there are problems17/07 08:46
comietekor just use the members17/07 08:46
comieteknumForFunctions {{num}} = ...17/07 08:46
comieteksorry, I made a typo earlier17/07 08:47
comietek{{..}} should have been {{...}} and that is literal syntax17/07 08:47
comietekI'm not sure if you'll be able to get what you want; the solver is a bit fickle17/07 08:48
comietekit may be that when you go on to define some function that would like to use the instance for (A -> A), other instances will also be in scope17/07 08:48
comietekand then Agda will complain17/07 08:49
comietekbut I'm not sure if that'll necessarily happen17/07 08:49
comietekyou can control this to some extent by defining instances in modules17/07 08:49
petercommandcomietek: ok, thanks, I will try that17/07 08:53
petercommandseems that I cannot do: overlap instance numForFunctions :  {A : Set} {{_ : Num A}} -> Num (A -> A)17/07 08:57
comietekis that an error message?17/07 09:27
comietekif not, what is the code you used, and what is the error?17/07 09:27
petercommandcomietek: I am trying to see if I can get agda to choose one of the available instances, so I add the word "overlap" before "instance numForFunctions : ..."17/07 09:54
petercommandcomietek: and the error I get is Parse error17/07 09:54
comietekpetercommand: uh.17/07 10:17
comietekis "overlap" defined as an Agda keyword somewhere I'm not aware of?17/07 10:17
rntzyes, overlap is an agda keyword, for instance resolution purposes17/07 10:19
rntzlemme go find the docs17/07 10:19
rntzcomietek: http://agda.readthedocs.io/en/v2.5.2/language/record-types.html search for "overlap" in that page17/07 10:19
rntzpetercommand: what version of the agda compiler are you using? `agda --version`?17/07 10:20
comietekok, this seems new17/07 10:21
comietekI haven't used this17/07 10:21
comietekbut reading the docs quickly, I see that the overlap keyword applies to individual *fields* of a record17/07 10:22
rntzI think it is fairly new, yeah17/07 10:22
comietekand not instances, which are values of a record type17/07 10:22
comietekI'll bbl; lecture17/07 10:22
rntzoh yeah, "overlap instance numForFunctions" is not right, unless numForFunctions is a record field17/07 10:23
petercommandrntz: 2.5.117/07 11:01
petercommandthe doc is 2.5.2 though17/07 11:02
arjen-jonathanHi17/07 12:48
petercommandhi arjen-jonathan 17/07 13:04
arjen-jonathanI don't understand Agda's sized types / how to define coinductive data-types with it17/07 16:13
arjen-jonathanWhat's the best resource to get to understand it?17/07 16:14
Saizanarjen-jonathan: http://www2.tcs.ifi.lmu.de/~abel/kyoto16/html/SizedTypes.html#1 <- small example17/07 16:57
Saizanhttp://www2.tcs.ifi.lmu.de/~abel/pc16/html/CopatternsSolution.html <- more17/07 17:02
arjen-jonathanSaizan: thanks!17/07 17:23

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