[Haskell-cafe] Two mysteries

[Tom Ellis]

On Sun, Aug 28, 2022 at 09:36:56AM -0700, Henry Laxen wrote:
> class State a  where
>   type StateKey   a :: *
>   type StateValue a :: *
>   lensTmap          :: Functor f => Lenstype f a (TMap (StateKey a) (StateValue a))
>   lensKey           :: Functor f => Lenstype f a (StateKey a)
>   lensCounter       :: Functor f => Lenstype f (StateValue a) Int
> 
> bump1 :: IO ()
> bump1 = do
>   xss <- makeSampleState
>   let xTmap = xss ^. tMap
>   withKey "a" (\(Just x) -> x & counter %~ (+1)) xTmap
>   print xTmap
>   
> -- Everything here is tickety-boo  
> -- λ> bump1
> -- TMap TVar: fromList [("a",TVar: SampleValue {_counter = 2, _other = ()})]
> 
> -- THE SECOND MYSTERY: now lets try bump1 with the type family, but there is no joy
> 
> -- bump2 :: IO ()
> -- bump2 = do
> --   xss <- makeSampleState
> --   let xTmap = xss ^. lensTmap
> --   withKey "a" (\(Just x) -> x & lensCounter %~ (+1)) xTmap
> --   print xTmap

This one is fairly easy to explain: `lensCounter` is a function that
can work for each `a` that is an instance of `State`.  So, the
`lensCounter` for which `a` should it be using here?

You think `a` should be `SampleState` because you've defined the
following instance, and you are trying to use `lensCounter` on a value
of type `SampleValue`.

> instance State SampleState where
>   type StateKey SampleState   = String
>   type StateValue SampleState = SampleValue
>   lensTmap        =  tMap
>   lensKey         =  key
>   lensCounter     =  counter
	  
But, suppose someone had also defined the following instance

> instance State () where
>   type StateKey ()   = String
>   type StateValue () = SampleValue
>   lensTmap        =  anotherTMap
>   lensKey         =  anotherKey
>   lensCounter     =  anotherCounter

When it comes to determine what `lensCounter` to use, `anotherCounter`
would work equally well as `counter`, as would the `lensCounter` of
_any_ `State` instance `a` for which `StateValue a = SampleValue`.
There's no unique choice to be made here, so type checking can't
proceed.

There are various ways to get around this, for example making `State`
a multiparameter type class and adding functional depencies. Perhaps
the following will work:

> class State a k v | a -> k, a -> v where
>   lensTmap          :: Functor f => Lenstype f a (TMap k v)
>   lensKey           :: Functor f => Lenstype f a k
>   lensCounter       :: Functor f => Lenstype f v Int
>
> instance State SampleState String SampleValue where
>   lensTmap        =  tMap
>   lensKey         =  key
>   lensCounter     =  counter

Tom