"Пропала планета" (C) Spaceballs

[thesz]

http://ect.bell-labs.com/who/ajeffrey/agda-frp-js/clock.html

Программка на Агде, показывает какое-то текущее время с помощью HTML5.

Исходнички.

Пришло по списку рассылки Агды, пока самого письма в Интернете нет.

Comments

[ex_juan_gan]

Clock

A clock

[thesz]

Что же из этого следует?

[ex_juan_gan]

А не видно агды. Виден джаваскрипт.

[kurilka]

"ECMAScript back end for Functional Reactive Programming in Agda", не?

[thedeemon]

clock : ⟦ Beh DOM ⟧
clock = element "p" (text (map toUTCString (every (1 sec))))

main : Main
main = reactimate clock

Подразумевалось, что часы будут идти и время меняться каждую секунду? Дык, не работает. Статично все.

[kurilka]

у меня работает

[kurilka]

небось JS отрубил? :)

[thedeemon]

нет, js включен, все остальные сайты пашут нормально.

[geniepro]

В Хроме пашет, а в Опере нет, видно нет там HTML5.
Посмотрел на исходник этого скрипта
http://ect.bell-labs.com/who/ajeffrey/agda-frp-js/require.js
страх и ужас ))

[kurilka]

неприязнь к require.js?

[nivanych]

Я тоже испытываю глубокую личную неприязнь к require.js...
Что же мне делать, ведь оно такое полезное, позволяет в некоторых бравзерах показывать часы...

[thesz]

Завидно?

[miserakl]

Правильно ли я понял, что все agda.frp.*.js написаны руками, а не сгенерированы? А во всех agda-файлах большая часть кода --- страхолюдный джаваскрипт в прагмах {-# COMPILED_JS ... #-}
Раз так, то планета ещё не пропала :(

[thesz]

О, не знаю, не смотрел.

Если они так сделали, то это неправильно, можно было бы сделать лучше.

И всё идёт к пропаже планеты. ;)

[miserakl]

Лучше --- это с помощью {-# COMPILED_JS ... #-} сделать привязки только самые низкоуровневые?

Всё идёт, но пока не пришло, а очень хочется. (Собственно, хочется простой вещи: есть функция f :: A -> B, где (JSON A, JSON B), хочется иметь javascript-функцию, преобразующую toJson (x :: A) в toJson (f x :: B). Если бы показали, как делать такое, было бы намного больше пользы, чем от фреймворка, который никуда не вставишь.)

[thesz]

>Собственно, хочется простой вещи: есть функция f :: A -> B, где (JSON A, JSON B), хочется иметь javascript-функцию, преобразующую toJson (x :: A) в toJson (f x :: B). Если бы показали, как делать такое, было бы намного больше пользы, чем от фреймворка, который никуда не вставишь.

Я не понял постановки задачи.

Что такое, например, "где (JSON A, JSON B)"?