From 899d8c460d0e765255863b35af185010711dca3c Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Tue, 30 Apr 2019 11:22:40 -0400
Subject: [PATCH] hash tables

---
 racket/typed/core-types.rkt   |  4 ---
 racket/typed/hash.rkt         | 68 +++++++++++++++++++++++++++++++++++
 racket/typed/roles.rkt        |  3 ++
 racket/typed/tests/hashes.rkt | 34 ++++++++++++++++++
 4 files changed, 105 insertions(+), 4 deletions(-)
 create mode 100644 racket/typed/hash.rkt
 create mode 100644 racket/typed/tests/hashes.rkt

diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt
index ef33880..6fbbdc1 100644
--- a/racket/typed/core-types.rkt
+++ b/racket/typed/core-types.rkt
@@ -714,13 +714,10 @@
      [(~Discard _)
       #t]
      [(X:id Y:id)
-      #;(printf "id case!\n")
       (free-identifier=? #'X #'Y)]
      [((~∀ (X:id ...) τ1) (~∀ (Y:id ...) τ2))
       #:when (stx-length=? #'(X ...) #'(Y ...))
       #:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2)
-      #;(printf "in ∀!\n")
-      #;(printf "τ2-X/Y = ~a\n" #'τ2-X/Y)
       (<: #'τ1 #'τ2-X/Y)]
      [((~Base τ1:id) (~Base τ2:id))
       (free-identifier=? #'τ1 #'τ2)]
@@ -744,7 +741,6 @@
            #t]))]
      ;; TODO: clauses for Roles, and so on
      [_
-      #;(printf "ids? ~a, ~a\n" (identifier? t1) (identifier? t2))
       #f]))
 
  ;; shortcuts for mapping
diff --git a/racket/typed/hash.rkt b/racket/typed/hash.rkt
new file mode 100644
index 0000000..586fdbd
--- /dev/null
+++ b/racket/typed/hash.rkt
@@ -0,0 +1,68 @@
+#lang turnstile
+
+(provide Hash
+         (for-syntax ~Hash)
+         hash
+         hash-set
+         hash-ref
+         hash-has-key?
+         hash-update
+         hash-remove
+         hash-map
+         hash-keys
+         hash-values
+         hash-keys-subset?
+         hash-count
+         hash-empty?
+         hash-union
+         )
+
+(require "core-types.rkt")
+(require (only-in "list.rkt" List))
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Immutable Hash Tables
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-container-type Hash #:arity = 2)
+
+(begin-for-syntax
+  (define-splicing-syntax-class key-val-list
+    #:attributes (items)
+    (pattern (~seq k1 v1 rest:key-val-list)
+             #:attr items #`((k1 v1) #,@#'rest.items))
+    (pattern (~seq)
+             #:attr items #'())))
+
+(define-typed-syntax (hash keys&vals:key-val-list) ≫
+  #:with ((key val) ...) #'keys&vals.items
+  [⊢ key ≫ key- (⇒ : τ-k)] ...
+  [⊢ val ≫ val- (⇒ : τ-val)] ...
+  #:fail-unless (all-pure? #'(key- ... val- ...)) "gotta be pure"
+  #:with together-again (stx-flatten #'((key- val-) ...))
+  --------------------------------------------------
+  [⊢ (hash- #,@#'together-again) (⇒ : (Hash (U τ-k ...) (U τ-val ...)))])
+
+(require/typed racket/base
+  ;; don't have a type for ConsPair
+  #;[make-hash : (∀ (K V) (→fn (List (ConsPair K V)) (Hash K V)))]
+  [hash-set : (∀ (K V) (→fn (Hash K V) K V (Hash K V)))]
+  [hash-ref : (∀ (K V) (→fn (Hash K V) K V))]
+  ;; TODO hash-ref/failure
+  [hash-has-key? : (∀ (K V) (→fn (Hash K V) K Bool))]
+  [hash-update : (∀ (K V) (→fn (Hash K V) (→fn V V) K (Hash K V)))]
+  ;; TODO hash-update/failure
+  [hash-remove : (∀ (K V) (→fn (Hash K V) K (Hash K V)))]
+  [hash-map : (∀ (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
+  [hash-keys : (∀ (K V) (→fn (Hash K V) (List K)))]
+  [hash-values : (∀ (K V) (→fn (Hash K V) (List V)))]
+  ;; TODO hash->list makes cons pairs
+  #;[hash->list : (∀ (K V) (→fn (Hash K V) (List (ConsPair K V))))]
+  [hash-keys-subset? : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) Bool))]
+  [hash-count : (∀ (K V) (→fn (Hash K V) Int))]
+  [hash-empty? : (∀ (K V) (→fn (Hash K V) Bool))])
+
+(require/typed racket/hash
+  [hash-union : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
+  ;; TODO - hash-union with #:combine
+  )
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 061cca3..07fec22 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -39,6 +39,8 @@
          (all-from-out "set.rkt")
          ;; sequences
          (all-from-out "sequence.rkt")
+         ;; hash tables
+         (all-from-out "hash.rkt")
          ;; DEBUG and utilities
          print-type print-role
          ;; Extensions
@@ -54,6 +56,7 @@
 (require "set.rkt")
 (require "prim.rkt")
 (require "sequence.rkt")
+(require "hash.rkt")
 
 (require (prefix-in syndicate: syndicate/actor-lang))
 
diff --git a/racket/typed/tests/hashes.rkt b/racket/typed/tests/hashes.rkt
new file mode 100644
index 0000000..d2c4571
--- /dev/null
+++ b/racket/typed/tests/hashes.rkt
@@ -0,0 +1,34 @@
+#lang typed/syndicate/roles
+
+(require rackunit/turnstile)
+
+(check-type (hash) : (Hash (U) (U)))
+
+(check-type (hash 1 2) : (Hash Int Int))
+
+(check-type (hash "greetings" 8) : (Hash String Int))
+
+(check-type (hash "smelly" 0
+                  "feet" 18
+                  "robust" 9)
+            : (Hash String Int))
+
+(check-type (hash "smelly" 0
+                  "feet" "grosss"
+                  "robust" #t)
+            : (Hash String (U Int String Bool)))
+
+(define a-hash
+  (hash "smelly" 0
+        "feet" 18
+        "robust" 9))
+
+(define hash-ref/inst (inst hash-ref String Int))
+
+(check-type (hash-ref/inst a-hash "smelly")
+            : Int
+            ⇒ 0)
+
+(check-type ((inst hash-count String Int) a-hash)
+            : Int
+            ⇒ 3)