From c9563cd0a2f2fe342a6e38f1f29c9c7ee3419dae Mon Sep 17 00:00:00 2001
From: Sam Caldwell <samc@ccs.neu.edu>
Date: Mon, 29 Apr 2019 17:03:39 -0400
Subject: [PATCH] type abstractions

---
 racket/typed/core-types.rkt        | 59 ++++++++++++++++++++++++++++--
 racket/typed/roles.rkt             |  4 +-
 racket/typed/tests/expressions.rkt | 36 ++++++++++++++++++
 3 files changed, 94 insertions(+), 5 deletions(-)
 create mode 100644 racket/typed/tests/expressions.rkt

diff --git a/racket/typed/core-types.rkt b/racket/typed/core-types.rkt
index 150ea9c..35cef8e 100644
--- a/racket/typed/core-types.rkt
+++ b/racket/typed/core-types.rkt
@@ -194,7 +194,10 @@
 (define-container-type AssertionSet #:arity = 1)
 (define-container-type Patch #:arity = 2)
 
+;; functions and type abstractions
+(define-binding-type ∀)
 (define-type-constructor → #:arity > 0)
+
 ;; for describing the RHS
 ;; a value and a description of the effects
 (define-type-constructor Computation #:arity = 4)
@@ -230,11 +233,11 @@
 (define-type-alias ⊥ (U*))
 
 (define-for-syntax (prune+sort tys)
-  (stx-sort 
-   (filter-maximal 
+  (stx-sort
+   (filter-maximal
     (stx->list tys)
     typecheck?)))
-  
+
 (define-syntax (U stx)
   (syntax-parse stx
     [(_ . tys)
@@ -245,6 +248,22 @@
          (stx-car #'tys-)
          (syntax/loc stx (U* . tys-)))]))
 
+(define-simple-macro (→fn ty-in ... ty-out)
+  (→ ty-in ... (Computation (Value ty-out)
+                            (Endpoints)
+                            (Roles)
+                            (Spawns))))
+
+(begin-for-syntax
+  (define-syntax ~→fn
+    (pattern-expander
+     (syntax-parser
+       [(_ ty-in:id ... ty-out)
+        #'(~→ ty-in ... (~Computation (~Value ty-out)
+                                      (~Endpoints)
+                                      (~Roles)
+                                      (~Spawns)))]))))
+
 ;; for looking at the "effects"
 (begin-for-syntax
   (define-syntax ~effs
@@ -694,6 +713,15 @@
            (<: #'τ-out1 #'τ-out2))]
      [(~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)]
      [((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...))
@@ -715,7 +743,9 @@
           [(== irrelevant)
            #t]))]
      ;; TODO: clauses for Roles, and so on
-     [_ #f]))
+     [_
+      #;(printf "ids? ~a, ~a\n" (identifier? t1) (identifier? t2))
+      #f]))
 
  ;; shortcuts for mapping
  (define ((<:l l) r)
@@ -1093,6 +1123,27 @@
                                                          (Endpoints τ-ep ...)
                                                          (Roles τ-f ...)
                                                          (Spawns τ-s ...))))])
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Type Abstraction
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define-typed-syntax (Λ (tv:id ...) e) ≫
+  [([tv ≫ tv- :: #%type] ...) () ⊢ e ≫ e- ⇒ τ]
+  --------
+  ;; can't use internal mk-∀- constructor here
+  ;; - will cause the bound-id=? quirk to show up
+  ;;   (when subsequent tyvar refs are expanded with `type` stx class)
+  ;; - requires converting type= and subst to use free-id=?
+  ;;   (which is less performant)
+  [⊢ e- ⇒ (∀ (tv- ...) τ)])
+
+(define-typed-syntax inst
+  [(_ e τ:type ...) ≫
+   [⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
+   #:fail-unless (pure? #'e-) "expression must be pure"
+   --------
+   [⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]]
+  [(_ e) ≫ --- [≻ e]])
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;; Sequencing & Definitions
diff --git a/racket/typed/roles.rkt b/racket/typed/roles.rkt
index 1fd97a5..dd19f88 100644
--- a/racket/typed/roles.rkt
+++ b/racket/typed/roles.rkt
@@ -8,11 +8,12 @@
          ;; Start dataspace programs
          run-ground-dataspace
          ;; Types
-         Int Bool String Tuple Bind Discard → ByteString Symbol
+         Int Bool String Tuple Bind Discard → ∀ ByteString Symbol
          Role Reacts Shares Know ¬Know Message OnDataflow Stop OnStart OnStop
          FacetName Field ★/t
          Observe Inbound Outbound Actor U
          Computation Value Endpoints Roles Spawns
+         →fn
          ;; Statements
          let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
          when unless send! define
@@ -22,6 +23,7 @@
          assert on field
          ;; expressions
          tuple select lambda ref observe inbound outbound
+         Λ inst
          ;; making types
          define-type-alias
          define-constructor define-constructor*
diff --git a/racket/typed/tests/expressions.rkt b/racket/typed/tests/expressions.rkt
new file mode 100644
index 0000000..241474e
--- /dev/null
+++ b/racket/typed/tests/expressions.rkt
@@ -0,0 +1,36 @@
+#lang typed/syndicate/roles
+
+(require rackunit/turnstile)
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;; Type Abstraction
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+
+(define id
+ (Λ [τ]
+   (lambda ([x : τ])
+     x)))
+
+(check-type id : (∀ (τ) (→fn τ τ)))
+
+(check-type ((inst id Int) 1)
+            : Int
+            ⇒ 1)
+(check-type ((inst id String) "hello")
+            : String
+            ⇒ "hello")
+
+(define poly-first
+  (Λ [τ σ]
+     (lambda ([t : (Tuple τ σ)])
+       (select 0 t))))
+
+(check-type poly-first : (∀ (A B) (→fn (Tuple A B) A)))
+
+(check-type ((inst poly-first Int String) (tuple 13 "XD"))
+            : Int
+            ⇒ 13)
+
+(check-type ((inst poly-first Int String) (tuple 13 "XD"))
+            : Int
+            ⇒ 13)