I’m not entirely sure what you mean.

AFRP was the original name of Yampa.

Yampa is embedded within Haskell, so much of its syntax is Haskell syntax.
One could embed Yampa, or a Yampa-like FRP language in Agda. The notation will differ slightly, as Agda has some syntactic differences from Haskell. There aren’t any Agda implementations suitable for FRP programming at the moment (that I am aware of), though I have used Agda to prototype several FRP variants with extended type-systems.

However, the above post was about defining the semantics of FRP, not its implementation.

In the Haskell embedding, Yampa makes use of the Arrows Framework, and the Arrow Notation that GHC supplies to go with it. To use the Arrow Notation you need to use the appropriate GHC extension:

{-# LANGUAGE Arrows #-}

Agda doesn’t provide Arrows in its standard library, but they can easily be defined. The Arrow Notation on the other hand would be harder, though something close should be possible as Agda is pretty liberal in terms of user-definable syntax.

Sorry if my question is particulary stupid, but I’ve just started using Yampa and I stil a bit cunfused about notation.

Bye.

Alba.

As a quick guide:

`Set’ is similar to kind `*’ in Haskell.

Datatypes are defined GADT style.

There’s no restrictions on the use of upper and lower case letters, but I tend to capitalise the first letter of type constructors.

A dependent function of type:

(s : Time) -> (s < = t) -> A

is similar to a non-dependent function of type:

Time -> A

with the constraint that the Time argument must be less than or equal to `t’. ((s <= t) is the type of proofs that the value `s’ is indeed less than or equal to the value `t’. The dependent version of the function requires this proof as an additional argument)

Additionally, I also avoid the problem of “rewriting history”, because the interface I allow is inherently point-wise, also in the output. Another consequence is that time delay can’t be expressed using this interface, but I’m not sure that’s a bad thing.

http://www.ee.bgu.ac.il/~noamle/_downloads/gaccum.pdf

Unfortunately I can’t understand most of the post (is this in Agda? Is it possible to summarize the constraints with traditional mathematical notations?)

My approach is more limiting, I am not only prohibiting systems to causality – but also to not being able to access values at arbitrary times (even if it’s the past). On the other hand I do want to allow “memory-full” operations. The only way I found to do this is by considering the *interface* I would like the semantic model of signal functions to have. I’ve yet to find a model that naturally imposes the above limitation, but allows memory-full operations. See the above report for more details

- Noam