search

tuura / plato

A DSL for asynchronous circuits specification
Other
12 stars 2 forks source link

WIP: Signal types #24

Closed snowleopard closed 8 years ago

snowleopard commented 8 years ago

This is a work in progress on type-safe signals.

mvdan commented 8 years ago

To make it easier to differentiate between PRs which are ready to merge and those which aren't, you usually prefix the title with WIP: like on mine :)

If I understand this correctly, a can be of any type?

snowleopard commented 8 years ago

WIP

Done! :)

If I understand this correctly, a can be of any type?

Yes, you are right. I do not put any constraints on the underlying representation of signals. However, in some cases we do ask for Eq a, Show a and other instances to be able to compare, show signals, etc.

mvdan commented 8 years ago

Yes, you are right. I do not put any constraints on the underlying representation of signals. However, in some cases we do ask for Eq a, Show a and other instances to be able to compare, show signals, etc.

Could we use this to somehow limit these to singletons of some kind? Like you could define "a" as a signal once, but not twice.

snowleopard commented 8 years ago

Each signal name like name = "a" can be defined at most once in Haskell, but there is no way to limit the number of times it can be used in other expressions. So, it may be used as part of both Input name and Output name. I don't think we can easily forbid this unfortunately.

mvdan commented 8 years ago

What if we simply iterated over the signals defined by the user and checked that the values made up a set, i.e. no repetitions?

You can argue this won't show up at compile time. But in the end we'd be compiling at runtime, so this would be a check that would run right after the compiling.

snowleopard commented 8 years ago

Well, the whole point of going through GADTs is to provide signal type checking at compile time. If we give it up, we can simply use data Signal a = Input a | Output a constructor that will work fine for runtime checks. /cc #17

mvdan commented 8 years ago

What should we do with this? I'm inclined to think that we should close it after the idea you had with wrappers. Circuits should take a number of arguments, and then the wrapping functions will let users easily make use of them with their own signal types.

snowleopard commented 8 years ago

Agreed, let me close this. I'll probably keep the branch for a while, it's an interesting experiment.