Email Gateway (Aug 19 2022 at 11:03): Email Gateway (Aug 19 2022 at 11:03):From: "Roger H." <s57076@hotmail.com>
Hello,
thank you Rene and Andreas for the help with the countable datatype, it works for a random type color.
Now my last problem is to show that the datatype --- 'a stream --- is countable.
Stream is a package in the FOCUS library and is smth defined with the HOLCF "domain" construct and resembles
the lists in Haskell. To show now:
instance stream :: (countable) countable
by.... ?
can you help me?
Many thanks!
Email Gateway (Aug 19 2022 at 11:03):From: René Thiemann <rene.thiemann@uibk.ac.at>
Dear Roger,
It definitely is not possible using the tactic mentioned by Andreas (which is based on
how "datatype"s are constructed by the datatype-package) and thus, also not by the wrapper
that makes use of this tactic in the "deriving" package.
So far I have never worked with HOLCF, but I just wondered whether you are sure that
stream really is countable: If it can model infinite lists (Haskell lists), then most
likely the set of all "bool stream"s already can encode the real interval [0,1] which is
uncountable.
Best regards,
René
Email Gateway (Aug 19 2022 at 11:03):From: Brian Huffman <huffman@in.tum.de>
René is right: The HOLCF stream type includes infinite lists and is
therefore uncountable (at least if the element type has cardinality >
1).
Last updated: Apr 25 2024 at 04:18 UTC