Is the class definition of `Dict` too restrictive? #17

Ptival · 2025-04-21T20:35:44Z

The definition of the Dict class mandates a ToIter (k ∧ x) (d x) superclass.

While this makes some sense, it prevents writing an instance for e.g.:

newtype PairDict k x = PairDict { getPairDict ∷ Dict k (x ∧ x) }

since its ToIter instance ought to look like ToIter (k ∧ (x ∧ x)) (Dict k x).

Unfortunately, the Haskell type system makes it unpleasant to try and introduce a type abstraction like:

class
  ( ...
  , ∀ x.                   ToIter (k ∧ v x) (d x)
  , ...
  ) ⇒ Dict k s d | d→k,d→s,d→v

since v cannot be the identity on types, or a non-fully-applied type synonym, which forces using a newtype like Identity, which makes everything worse.

I am locally testing out an approach where we would remove the item type of collections from the type of classes like ToIter, Single, etc., instead favoring an associated type family:

class Collection t where type Item t ∷ ★
class ToIter t where iter ∷ t → 𝐼 (Item t)

It seems to work, though it sometimes need to manipulate explicit type equalities to match was was once achieved via unification, e.g.:

exec ∷ (Monad m,ToIter (m ()) t) ⇒ t → m ()
-- becomes:
exec ∷ (Monad m,ToIter t,Item t ~ m ()) ⇒ t → m ()

It also highlights that there needs to be a different notion for items as can be inserted in the data structure, and items as can be retrieved from the data structure. For list-likes, these notions match, but for dict-likes, they are distinct:

Pairs (key, value) can be inserted,
But values can be looked up.
So you end up with:

class Collection t where
  -- | This is the type of items that can be inserted in the collection.  For instance, for a
  -- dictionary, it would be a pair of key-values.
  type InsertableItem t ∷ ★
  -- | This is the type of items that can be looked up in the collection.  For instance, for a
  -- dictionary, it would be just the values.
  type RetrievableItem t ∷ ★

class Single t where single ∷ InsertableItem t → t
class Lookup k t | t → k where (⋕?) ∷ t → k → 𝑂 (RetrievableItem t)
class Access k t | t → k where (⋕) ∷ t → k → RetrievableItem t

I am still working out the details of how such a change would alter the type signature of the Dict class, it's definitely quite the change, so might not be desirable.

There is an also in-between approach where we leave ToIter and such as they are, and bring the associated type family only for Dict, if that would be more acceptable.

The text was updated successfully, but these errors were encountered:

davdar · 2025-04-21T20:57:06Z

Can you say more about why you are wanting a type like this:

newtype PairDict k x = PairDict { getPairDict ∷ Dict k (x ∧ x) }

to fit an interface like this?

class
  ( ...
  , ∀ x.                   ToIter (k ∧ v x) (d x)
  , ...
  ) ⇒ Dict k s d | d→k,d→s,d→v

Also happy to chat on a call if that's less time consuming for you.

davdar · 2025-04-21T20:58:56Z

Ah, I take it the Dict you're referring to is the one from here? https://uvm-plaid.github.io/uvmhs/uvmhs-0.0.0.0/UVMHS-Core-Data-Dict.html

davdar · 2025-04-21T20:59:31Z

I think I am getting it now.

Ptival · 2025-04-21T20:59:36Z

This just started with wanting to use the overloaded ⩌ for the wrapped type.

davdar · 2025-04-21T21:00:53Z

Ok let's chat about this, tomorrow, and quickly, if possible :)

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Is the class definition of `Dict` too restrictive? #17

Is the class definition of `Dict` too restrictive? #17

Is the class definition of Dict too restrictive? #17

Is the class definition of Dict too restrictive? #17

Comments

Is the class definition of `Dict` too restrictive? #17

Is the class definition of `Dict` too restrictive? #17