Jake (Oct 13 2022 at 03:39): Jake (Oct 13 2022 at 03:39):New-user question: what's the best way to express types with a lot of dependent information? I've been using specifications, which are great when you have a single condition or a single extra piece of data, but they start to get really verbose when you have a lot of data types all depending on each other.
For example, I'm trying to formalize a Boolean circuit, which is something like: "a DAG with a function that maps nodes of the DAG to gate types, such that exactly n of those gates are input gates, and those input gates have a function to the naturals that is injective over the first n naturals..." etc.
Pierre Courtieu (Oct 13 2022 at 08:42):I guess the nominal answer is: a dependent record. But that is not the end of the story. Whether the record should be declared as a type class or whatever should be discussed. But you should definitely start with a record.
Jake (Oct 13 2022 at 12:30):That looks like exactly what I was looking for. Thanks! I'll give it a try.
Notification Bot (Oct 13 2022 at 12:30):Jake has marked this topic as resolved.
Last updated: Oct 03 2023 at 20:01 UTC