Stream: Beginner Questions

Topic: Recursive datatype sets bnf


view this post on Zulip Bernhard Stöckl (Sep 20 2021 at 14:07):

I'm trying to use a recursive datatype that uses sets like this:
datatype 'a test = Test 'a "('a test) set"
But this results in the error

Unsupported recursive occurrence of type "'a test" via type constructor "Set.set" in type expression "'a test set"
Use the "bnf" command to register "Set.set" as a bounded natural functor to allow nested (co)recursion through it

If I use "list" or "fset" instead of "set" it works. But is there a way to do this with normal sets or should I just use fsets instead?

view this post on Zulip Dmitriy Traytel (Sep 20 2021 at 16:11):

If this was allowed, Test x :: 'a test set => 'a test would be a total, injective function from the the powerset of a set to the set. You could prove False from that easily.

The BNF abstraction is what separates types that may nest recursive occurrences from those which may not. The types of lists and finite sets are BNFs, but "'a set" isn't.


Last updated: Jul 15 2022 at 23:21 UTC