Finite types can be ordered

[treeowl]

Every finite type can be ordered (somehow). Here's one way to express that:

class (Universe a, Coercible a (Ordered a), Ord (Ordered a)) => Finite a where
  type Ordered a
  type Ordered a = a

  universeS :: Set (Ordered a)
  universeS = fromList (coerce $ universeF @a)

  universeF :: [a]
  universeF = coerce . toList $ universeS @a

Another option would be to allow an arbitrary Iso' between a and a (possibly very different) Ordered a, which might be better if the ordering on Ordered a can't be expressed efficiently by directly comparing elements of a.

class (Universe a, Ord (Ordered a)) => Finite a where
  type Ordered a
  type Ordered a = a

  ordering :: Iso' a (Ordered a)
  default ordering :: Coercible a (Ordered a) => Iso' a (Ordered a)
  ordering = coerced

  universeS :: Set (Ordered a)
  universeS = fromList (map (view ordering) (universeF @a))

  universeF :: [a]
  universeF = universe

-- A default definition of `universe` or `universeF` in terms of `universeF`
universeFfromS :: forall a. Finite a => [a]
universeFfromS = map (view (from ordering)) . toList $ universeS @a

[phadej]

What are you proposing?

[treeowl]

@phadej, I'm proposing to add the ability to make a Set representing a finite universe, in a reasonably efficient manner. There's an inefficient way to do it:

newtype DefaultFiniteOrdered a = DO Int deriving (Eq, Ord)

defaultFiniteOrdering :: Finite a => Iso' a (DefaultFiniteOrdered a)
defaultFiniteOrdering = iso f g
  where
    f a = DO (fromJust (elemIndex a universeF))
    g (DO i) = universeF !! i

[phadej]

I think I lack some context

[phadej]

I'm also worried about adding something as strict as Set to Finite.

Int is Finite. The dictionary containing universeF :: [Int] is kind-of space leak, as it's probably never GCd, but luckily only used part leaves on the heap. With Set users would be very careful with Finite usage.

I understand that its also often useful to have something like [minBound .. maxBound] but more principled, but I don't know how to separate "Finite" and "fits into memory". Former composes, latter doesn't.

[dmwit]

Users who want this can do it themselves, though, right?

newtype MyOrdering = MyOrdering Foo
instance Eq Foo where ...
instance Ord Foo where ...
instance Finite MyOrdering where universeF = coerce (universeF :: Foo)
universeS = S.fromList universeF

Is that actually more code than what they would have to do with your proposal? It seems like it can't be much more than one or two extra lines, if any; the instance Eq and instance Ord bits are going to be the verbose ones, and they have to be there in both proposals (along with the newtype), which only leaves a maximum difference of two lines of code.