Safe Functional Reactive Programming though Dependent Types

Accompanying code for the paper Safe Functional Programming though Dependent Types can be accessed here. You can either download the Agda source files, or browse them as html. There is also a related Haskell implementation that encodes decoupledness using Type Families. This implementation diverges somewhat from the paper, but provides greater functionality.

There are three Agda versions available:

The first version (icfp09) corresponds to the semantics given in the paper, but does not include uninitialised signals.
The second version (icfp09Full) is the full implementation including uninitialised signals. icfp09 is far simpler and more readable, as the presence of uninitialised signals requires quite a lot of coercing of signals, along with accompanying proofs to ensure this is safe. They also require a separate evaluation function for time zero.
The third version (icfp09Set1) is a basic implementation that does not use the "type-in-type" Agda option. The disadvantage of this version is duplicated and ugly code (as Agda does not support universe polymorphism), but it does avoid any issues about the "type-in-type" flag making Agda unsound. The main purpose of this version is to demonstrate that we can translate the other implementations (to avoid using the "type-in-type" flag) in a straightforward and mechanical fashion, and that we're not exploiting the unsoundness of this option.

Implementation Without Uninitialised Signals (icfp09)

Last updated 2nd July 2024.