Stream: Coq users

Topic: ✔ Complicated dependent types

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Jake (Oct 13 2022 at 12:30):

That looks like exactly what I was looking for. Thanks! I'll give it a try.

view this post on Zulip Notification Bot (Oct 13 2022 at 12:30):

Jake has marked this topic as resolved.

Last updated: May 20 2024 at 20:01 UTC