map.lean

import Std.Data.HashMap

open Std

/-
In Lean, a hash map has type

def HashMap (α : Type u) (β : Type v) [BEq α] [Hashable α] :=
  ...

The square brackets are used to mark implicit arguments that must be inferred using type class resolution.

- `BEq α` is the type class for types `α` that have an operation `beq : α → α → Bool` that is an equivalence relation.
   The `B` is for Boolean equality. We use `a == b` as notation for `BEq.beq a b`.
   In Lean, `a = b` is a proposition, and is notation `Eq a b`. 

- `Hashable α` is the type class for types `α` that have an operation `hash : α → UInt64`

Lean has 3 different kinds of binder annotations.

- Explicit argument: example `(α : Type u)`
- Implicit argument that must be inferred using type class resolution:  example `[Hashable α]`. This is equivalent to
  the type class arguments that occur before `=>` in Haskell. In Lean, we don't use the Haskell approach because we
  sometimes have type class implicit arguments that depend on explicit arguments
- Implicit arguments that are inferred using typing constraints. For example the identity function can be written as
  ```
  def id {α : Type} (a : α) := a
  ```
We also support Haskell compact style where just write
```
  def id (a : α) := a
```
Idris uses a similar approach.
-/


#check HashMap String Nat -- HashMap String Nat : Type

set_option pp.explicit true in
#check HashMap String Nat 
  -- @HashMap String Nat (@instBEq String fun (a b : String) => instDecidableEqString a b) instHashableString : Type

/-
Two possible styles to define functions on HashMaps.
-/

/-
In the following style, Lean generates the instances `BEq` and `Hashable` whenever we write
an `insert1` application. The typing rules will enforce that the inferred instances match the ones stored
in the type.
The header is equivalent to
```
insert1 [s1 : BEq α] [s2 : Hashable α] (m : @HashMap α β s1 s2) (a : α) (b : β) : HashMap α β
```
-/
def insert1 [BEq α] [Hashable α] (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
    m.insert a b

/-
In the following style, Lean infers the regular implicit arguments from the type of `m`.
The header is equivalent to
```
insert2 {s1 : BEq α} {s2 : Hashable α} (m : @HashMap α β s1 s2) (a : α) (b : β) : HashMap α β
```
-/
def insert2 {s1 : BEq α} {s2 : Hashable α} (m : HashMap α β) (a : α) (b : β) : HashMap α β :=
    m.insert a b

def ex : HashMap String Nat :=
  let m : HashMap String Nat := {} -- Empty hash map
  let m := insert1 m "john" 45
  let m := insert1 m "mary" 56
  m

#eval ex.toList -- [("john", 45), ("mary", 56)]

-- The following command defines a new instance `Hashable String`
instance (priority := high) : Hashable String where
  hash s := s.length.toUInt64

#check insert1 ex "leo" 49 -- Error application type mismatch

#check insert2 ex "leo" 49 -- Ok