How to properly create a HashMap from linear-base (Data.HashMap.Mutable.Linear) in Haskell?

Question

I was able to successfully make a HashMap from Data.HashMap.Mutable.Linear in the linear-base package, using the LinearTypes extension in GHC 9:

{-# LANGUAGE LinearTypes #-}

module Main where

import Data.HashMap.Mutable.Linear
import Data.Unrestricted.Linear

main :: IO ()
main = do
  let m :: (HashMap Int String %1 -> Ur b) %1 -> Ur b
      m = empty 10
  let m' = m (\h -> toList (insert 1 "s" (insert 2 "w" h)))
  let um = unur m'
  print um

This looks pretty unergonomic because the entire HashMap has to be created all in one go, and after it is created, I get a [(Int, String)]. I want to continue having the HashMap around to add, update, remove items, etc. In non-linear Haskell, using unordered-containers, it looks like:

module Main where

import Data.HashMap.Strict

main :: IO ()
main = do
  let m :: HashMap Int String
      m = empty
  let m1 = insert 1 "s" m
  -- anywhere else in the code...
  let m2 = insert 2 "w" m1
  print $ m2

I wrote the former entirely based on the types I can find in the documentation. empty seems to match the empty function for non-linear HashMaps, but it has type

empty :: forall k v b. Keyed k => Int -> (HashMap k v %1 -> Ur b) %1 -> Ur b

It says

Run a computation with an empty HashMap with given capacity.

My understanding is that I give it an Int as the capacity, and then a "computation" that transforms a HashMap into a Ur b. The only function I can find that satisfy that type is toList :: HashMap k v %1 -> Ur [(k, v)]. The other functions like insert (insert :: Keyed k => k -> v -> HashMap k v %1 -> HashMap k v) all return a new HashMap (which is actually what I'd expect, but empty requires me to return Ur b).

Ideally empty would return a HashMap instead of a Ur b, but returning Ur (HashMap ...) is fine for me too. There is a function with signature a -> Ur a, which is the Ur constructor, but if I replace toList with it, I get:

    • Couldn't match type ‘'Many’ with ‘'One’
        arising from multiplicity of ‘h’
    • In the first argument of ‘m’, namely
        ‘(\ h -> Ur (insert 1 "s" (insert 2 "w" h)))’
      In the expression: m (\ h -> Ur (insert 1 "s" (insert 2 "w" h)))
      In an equation for ‘m'’:
          m' = m (\ h -> Ur (insert 1 "s" (insert 2 "w" h)))
   |
24 |   let m' = m (\h -> Ur (insert 1 "s" (insert 2 "w" h)))
   |                ^

Answer 1

I think the idea is to move your interesting hash map computations into the continuation of empty, e.g. your second example would be written like this:

{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE NoImplicitPrelude #-}

module Main where

import Data.HashMap.Mutable.Linear
import Prelude.Linear hiding (insert)

main :: IO ()
main = print (unur $ empty 10 $ \m ->
  insert (1 :: Int) "s" m & \case
    -- anywhere else in the code...
    m -> insert 2 "w" m & \case
      m -> toList m)

It's not pretty, but here's what I meant with doing IO:

{-# LANGUAGE LinearTypes #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE UnboxedTuples #-}

module Main where

import Prelude ((*>))
import Data.HashMap.Mutable.Linear
import Prelude.Linear hiding (insert)

print' :: (Show k, Show v) => HashMap k v %1 -> Ur (IO ())
print' x = toList x & \(Ur x1) -> Ur (print x1)

main :: IO ()
main = unur $ empty 10 $ \m ->
  insert (1 :: Int) "s" m & \case
    m -> dup m & \case
      (m1, m) -> print' m1 & \case
        (Ur io1) -> insert 2 "w" m & \case
          m -> print' m & \case
            (Ur io2) -> Ur (io1 *> io2)

Arguably, this is equivalent to doing the IO outside of this function, so I don't know how useful this is.

I guess a better solution would be to have an empty function that explicitly allowed a form of IO.