Sets, typeclasses and functional dependencies
Hi Haskellers, After reading: https://stackoverflow.com/questions/34790721/where-is-the-set-type-class https://stackoverflow.com/questions/25191659/why-is-haskell-missing-obvious-... https://stackoverflow.com/questions/11508642/haskell-how-can-i-define-a-type... I can see why Haskell base does not provide typeclasses for sets. I'm wondering now though if I did create a Set typeclass what it would look like. There's several approaches using various language extensions and to me this approach using functional dependencies seems simpler than the other approaches: class Setish set a | set -> a where empty :: set singleton :: a -> set -- and so on. My question is how does the functional dependency in Setish interact with "extra" types needed for richer set operations like finding the powerset or taking a cartesian product? Something like: class Setish set a | set -> a where empty :: set singleton :: a -> set power_set :: set -> ?something product :: set -> ?something -> ?something -- and so on. TIA, Stu
On Sat, 31 Jul 2021, Stuart Hungerford wrote:
I can see why Haskell base does not provide typeclasses for sets. I'm wondering now though if I did create a Set typeclass what it would look like. There's several approaches using various language extensions and to me this approach using functional dependencies seems simpler than the other approaches:
class Setish set a | set -> a where
empty :: set
singleton :: a -> set
-- and so on.
A more modern approach would use type functions: class Setish set where type Element set empty :: set singleton :: Element set -> set
My question is how does the functional dependency in Setish interact with "extra" types needed for richer set operations like finding the powerset or taking a cartesian product?
powerset would need a type like: powerset :: (Powersettish powerset, Element powerset ~ set, Setish set) => set -> powerset with an extra Powersettish class. However, the type checker could not guess the exact powerset type, it could be, e.g. powerset :: Set a -> Set (Set a) or powerset :: Set a -> [Set a] If you want that the powerset type is determined by the set type, then you might define class Settish set where ... type Powerset set powerset :: set -> Powerset set
On Sat, Jul 31, 2021 at 7:14 PM Henning Thielemann <lemming@henning-thielemann.de> wrote:
[...] A more modern approach would use type functions:
class Setish set where type Element set empty :: set singleton :: Element set -> set
Thanks for the pointer.
My question is how does the functional dependency in Setish interact with "extra" types needed for richer set operations like finding the powerset or taking a cartesian product?
powerset would need a type like:
powerset :: (Powersettish powerset, Element powerset ~ set, Setish set) => set -> powerset
with an extra Powersettish class.
However, the type checker could not guess the exact powerset type, it could be, e.g. powerset :: Set a -> Set (Set a) or powerset :: Set a -> [Set a]
Okay, I'm starting to see why the "Set" typeclass examples I could find don't include a powerset or cartesian product method. Thanks again, Stu
The thing about powerset is that it is great for reasoning and as a starting point for a derivation, but horrible as a data structure. Power sets get very big very fast, and even in a lazy language, where you might not store an entire powerset, traversing one takes a lot of time. So it's seldom included in practical finite set implementations. On Sat, 31 Jul 2021 at 22:15, Stuart Hungerford <stuart.hungerford@gmail.com> wrote:
On Sat, Jul 31, 2021 at 7:14 PM Henning Thielemann <lemming@henning-thielemann.de> wrote:
[...] A more modern approach would use type functions:
class Setish set where type Element set empty :: set singleton :: Element set -> set
Thanks for the pointer.
My question is how does the functional dependency in Setish interact with "extra" types needed for richer set operations like finding the powerset or taking a cartesian product?
powerset would need a type like:
powerset :: (Powersettish powerset, Element powerset ~ set, Setish set) => set -> powerset
with an extra Powersettish class.
However, the type checker could not guess the exact powerset type, it could be, e.g. powerset :: Set a -> Set (Set a) or powerset :: Set a -> [Set a]
Okay, I'm starting to see why the "Set" typeclass examples I could find don't include a powerset or cartesian product method.
Thanks again,
Stu _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.
On Mon, Aug 2, 2021 at 12:29 PM Richard O'Keefe <raoknz@gmail.com> wrote:
The thing about powerset is that it is great for reasoning and as a starting point for a derivation, but horrible as a data structure. Power sets get very big very fast, and even in a lazy language, where you might not store an entire powerset, traversing one takes a lot of time. So it's seldom included in practical finite set implementations.
Very true, although there's something neat about being able to generate 2^{some set}. I'm mainly interested in doing the exercises in the "Haskell Road to Logic and Mathematics" with some added exploration, e.g. a Set typeclass. Stu
On 31/07/2021 11.14, Henning Thielemann wrote:
A more modern approach would use type functions:
class Setish set where type Element set empty :: set singleton :: Element set -> set
Just to add: This would be an "extensional" set, i.e one specified explicitly by its elements. But there are also "intensional" sets which are defined by some sort of mathematical property that holds for its elements. Naturally, the operations that make sense for either of those is *very* different.
participants (4)
-
Bardur Arantsson -
Henning Thielemann -
Richard O'Keefe -
Stuart Hungerford