Map: lookp return value type inference and multiple identical keys

[miguel-negrao]

In Map, if I write

myMap :: Map '[ "w" ':-> Int]
myMap = Ext (Var :: (Var "w")) 2 Empty

elemAtW = lookp (Var :: (Var "w")) myMap

GHC cannot deduce the type returned by lookp[1]. For my use case this makes Map not usable. My first reasoning was that this was strange as, as I thought that in a map there can only be one key of a certain value (in this case type), and for that map the associated value is Int.

But then I tried creating a map with multiple identical keys, and it works:

myMap2 :: Map '[ "w" ':-> Int, "w" ':-> Int]
myMap2 = Ext (Var :: (Var "w")) (2::Int) $ Ext (Var :: (Var "w")) (4::Int) Empty

I see that asMap would transform this back a proper map, summing 2 and 4. Still, in terms of type inference this means that GHC cannot ever deduce the type returned by lookp ? Would in theory be possible to have a different implementation of Map where duplicate keys were not allowed and GHC could infer the type returned by lookp ?

[1]

• Overlapping instances for IsMember "w" t0 '[ "w" ':-> Int]
    arising from a use of ‘lookp’
  Matching instances:
    two instances involving out-of-scope types
    (use -fprint-potential-instances to see them all)
  (The choice depends on the instantiation of ‘t0’
   To pick the first instance above, use IncoherentInstances
   when compiling the other instance declarations)
• In the expression: lookp (Var :: (Var "w")) myMap
  In an equation for ‘elemAtW’:
      elemAtW = lookp (Var :: (Var "w")) myMap

[dorchard]

Okay so there are two things going on here. In the myMap example, the problem is that 2 has an adhoc polymorphic type Num a => a so the type-families cannot compute the representation correctly. This is solved by adding the :: Int signature as you did in myMap2. I haven't found any way round this, and it tends to only be a problem with overloaded data like integers: the rest of the time a lookp can be inferred by GHC.

Regarding disallowing multiple keys when constructing. That is possibly if you use the asMap function on the definition of myMap2. I guess I could expose some smart constructors that also apply asMap for you? But I'd like to still keep the representation open.

[dorchard]

Added smart constructors. Hopefully that is enough?

[miguel-negrao]

Hi

Thanks for having a look at this.

In the myMap example, the problem is that 2 has an adhoc polymorphic type Num a => a so the type-families cannot compute the representation correctly. This is solved by adding the :: Int signature as you did in myMap2. I haven't found any way round this, and it tends to only be a problem with overloaded data like integers: the rest of the time a lookp can be inferred by GHC.

But adding the ::Int signature doesn't solve the issue:

myMap :: Map '[ "w" ':-> Int]
myMap = Ext (Var :: (Var "w")) (2::Int) Empty

-- doesn't compile
elemAtW = lookp (Var :: (Var "w")) myMap

and the problem is still present when using a non-polymorphic literal Char:

myMap5 :: Map '[ "w" ':-> Char]
myMap5 = Ext (Var :: (Var "w")) 'a' Empty

-- doesn't compile
elemAtW5 = lookp (Var :: (Var "w")) myMap5

The overlapping instances (shown using -fprint-potential-instances):

/home/miguel/Development/Haskell/projects/SC/tests/test-type-level-sets/Main.hs:13:11: error:
    • Overlapping instances for IsMember "w" t0 '[ "w" ':-> Int]
        arising from a use of ‘lookp’
      Matching instances:
        two instances involving out-of-scope types
          instance [overlappable] [safe] IsMember v t m =>
                                         IsMember v t (x : m)
            -- Defined in ‘Data.Type.Map’
          instance [overlap ok] [safe] IsMember v t ((v ':-> t) : m)
            -- Defined in ‘Data.Type.Map’
      (The choice depends on the instantiation of ‘t0’
       To pick the first instance above, use IncoherentInstances
       when compiling the other instance declarations)
    • In the expression: lookp (Var :: (Var "w")) myMap
      In an equation for ‘elemAtW’:
          elemAtW = lookp (Var :: (Var "w")) myMap

Added smart constructors. Hopefully that is enough?

For disallowing multiple keys when constructing, yes, I think so. It doesn't solve the issue of GHC not inferring the type, I still get the same error.

In the meantime for my application I switched to using records from the extensible package.

[jmorag]

For better inference, you can augment lookp with an extra constraint

lookp' :: (IsMember v t m, Just t ~ Lookup m v) => Var v -> Map m -> t
lookp' = lookp

which gives you

elemAtW5 = lookp' (Var :: (Var "w")) myMap5
-- 'a'

[dorchard]

okay interesting. @jmorag perhaps you could create a PR with this lookp' then? Would it make sense just to have this be the main definition of lookp perhaps?

[jmorag]

I think if we're changing code, a better solution is to add a functional dependency to IsMember

class IsMember v t m | m v -> t where
  lookp :: Var v -> Map m -> t

which has same nice inference properties as lookp'. I'll open a PR with this.