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

--- Day changed Mon May 01 2017
{AS}subttle: It is possible01/05 08:58
{AS}Basically you just wrap the record in a module01/05 08:59
{AS}and use open Record public01/05 09:00
{AS}inside the module01/05 09:00
{AS}and define your function there01/05 09:00
{AS}subttle: 01/05 09:04
{AS}https://www.irccloud.com/pastebin/pDzfFHrL/01/05 09:04
IredHi, I'm trying to do agda -> js compile, but can't seem to get a trivial structure to work :( maybe you can tell me what I'm missing.. 01/05 10:48
Iredmodule Try1 where  open import Agda.Builtin.List open import Agda.Builtin.String    e0 : List String e0 = []  e1 : List String e1 = "a" ∷ []01/05 10:49
Iredin js: _jAgdaTry.e0 function (x0) {     return x0["[]"]();   } _jAgdaTry.e0() jAgda.Agda.Builtin.List.js:11 Uncaught TypeError: Cannot read property '[]' of undefined01/05 10:49
Ired... line breaks are not getting through :)01/05 10:50
Ireddoes it make sense like this, or should I copy line-by-line? 01/05 10:51
Iredanyone awake here btw? 01/05 11:23
Ired:)01/05 11:23
Iredcan you help me with a simple agda -> js compile issue.. I must be missing something trivial here01/05 11:23
Iredmodule Try1 where01/05 11:24
Ired  open import Agda.Builtin.List01/05 11:24
Ired  open import Agda.Builtin.String01/05 11:25
Ired  e0 : List String01/05 11:25
Ired  e0 = []01/05 11:25
Ired  e1 : List String01/05 11:25
Ired  e1 = "a" ∷ []01/05 11:25
Ired---01/05 11:25
Iredcompiles to js, but the resulting module contains:01/05 11:26
Ired_jAgdaTry.e0   :01/05 11:27
Iredfunction (x0) {     return x0["[]"]();   }01/05 11:27
Iredshouldn't this be a constant? or at least a function needing no parameter?01/05 11:28
comieteklred: please use an online paste service such as gist.github.com01/05 11:32
Iredhttps://gist.github.com/anonymous/2c8a0ce1f68845bb9884cbc444e12a3501/05 11:35
{AS}Ired: My guess this is a function that accepts the module that defines "[]" and "[_::_]" as input01/05 11:56
{AS}Ired: In the same way that _jAgdaTry is a module which defines e0 and e101/05 11:56
{AS}Of course, one could wonder why they do not hard-code the module instead of parameterizing over it01/05 11:58
{AS}and to that I do not know the answer01/05 11:59
Iredhttps://gist.github.com/tiborveres-ired/86999c04fefb532391b35a470a1404b501/05 12:04
Iredadded a comment with the generated js files01/05 12:04
Iredlike the exported List.[] constructor expects a parameter with "[]" member01/05 12:06
Iredthat would somehow be (List String) ?01/05 12:06
{AS}Ired: JavaScript is untyped01/05 12:13
Iredtrue, but as this a result of agda -> js compilation some "typedness" bleeds over in the expectation for parameter structures.. 01/05 12:18
gallaisCould it have to do with making the generated output lazy?01/05 13:17
Iredgallais: you wrote this to me? can you elaborate? I just compiled with agda --js Try1.agda01/05 13:24
gallaisWell taking an extra (unit) argument is a common way to build a thunk01/05 14:20
gallaisSo this could just be a way to force lazyness01/05 14:20
IredI see, you're probably right; is there a "proper" way to disable this for a specific case ?01/05 14:44
subttle{AS}: Ah, perfect! Thanks!!01/05 15:08
gallaisI don't think so. Apart from patching the backend yourself.01/05 16:13
--- Log closed Mon May 01 17:42:29 2017
--- Log opened Mon May 01 17:42:37 2017
-!- Irssi: #agda: Total of 122 nicks [0 ops, 0 halfops, 0 voices, 122 normal]01/05 17:42
-!- Irssi: Join to #agda was synced in 120 secs01/05 17:44
mudriIs {-# TERMINATING #-} used to assert that a definition is productive?01/05 18:06

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