limited support for effect polymorphism
This commit is contained in:
parent
20693f234e
commit
99d5916bd1
|
@ -303,6 +303,50 @@
|
||||||
(~parse vars-pat #'())
|
(~parse vars-pat #'())
|
||||||
body-pat))])))))
|
body-pat))])))))
|
||||||
|
|
||||||
|
;; shorthand for writing function types
|
||||||
|
(define-syntax-parser proc
|
||||||
|
[(_ (~optional (~seq #:forall (X:id ...)))
|
||||||
|
ty-in ...
|
||||||
|
(~or (~datum ->) (~datum →))
|
||||||
|
ty-out
|
||||||
|
(~or (~optional (~seq #:spawns (s ...+)))
|
||||||
|
(~optional (~seq #:roles (r ...+)))
|
||||||
|
(~optional (~seq #:endpoints (e ...+))))
|
||||||
|
...)
|
||||||
|
#:with spawns (if (attribute s) #'(s ...) #'())
|
||||||
|
#:with roles (if (attribute r) #'(r ...) #'())
|
||||||
|
#:with endpoints (if (attribute e) #'(e ...) #'())
|
||||||
|
#:with body #`(→ ty-in ... (Computation (Value ty-out)
|
||||||
|
(Endpoints #,@#'endpoints)
|
||||||
|
(Roles #,@#'roles)
|
||||||
|
(Spawns #,@#'spawns)))
|
||||||
|
(if (attribute X)
|
||||||
|
#'(∀ (X ...) body)
|
||||||
|
#'body)])
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
(define-syntax ~proc
|
||||||
|
(pattern-expander
|
||||||
|
(syntax-parser
|
||||||
|
[(_ (~optional (~seq #:forall (X:id ...)))
|
||||||
|
ty-in ...
|
||||||
|
(~or (~datum ->) (~datum →))
|
||||||
|
ty-out
|
||||||
|
(~or (~optional (~seq #:spawns s))
|
||||||
|
(~optional (~seq #:roles r))
|
||||||
|
(~optional (~seq #:endpoints e)))
|
||||||
|
...)
|
||||||
|
#:with spawns (if (attribute s) #'(s) #'())
|
||||||
|
#:with roles (if (attribute r) #'(r) #'())
|
||||||
|
#:with endpoints (if (attribute e) #'(e) #'())
|
||||||
|
#:with body #`(~→ ty-in ... (~Computation (~Value ty-out)
|
||||||
|
(~Endpoints #,@#'endpoints)
|
||||||
|
(~Roles #,@#'roles)
|
||||||
|
(~Spawns #,@#'spawns)))
|
||||||
|
(if (attribute X)
|
||||||
|
#'(~∀ (X ...) body)
|
||||||
|
#'body)]))))
|
||||||
|
|
||||||
;; for looking at the "effects"
|
;; for looking at the "effects"
|
||||||
(begin-for-syntax
|
(begin-for-syntax
|
||||||
(define-syntax ~effs
|
(define-syntax ~effs
|
||||||
|
@ -591,6 +635,7 @@
|
||||||
(syntax-parse τ
|
(syntax-parse τ
|
||||||
[(~→ τ ...) #f]
|
[(~→ τ ...) #f]
|
||||||
[(~Actor τ) #f]
|
[(~Actor τ) #f]
|
||||||
|
[(~Role (_) _ ...) #f]
|
||||||
[_ #t]))
|
[_ #t]))
|
||||||
|
|
||||||
(define-for-syntax (strip-? t)
|
(define-for-syntax (strip-? t)
|
||||||
|
@ -736,9 +781,13 @@
|
||||||
[(_ nm:id)
|
[(_ nm:id)
|
||||||
#'((~literal #%plain-app) nm)])))
|
#'((~literal #%plain-app) nm)])))
|
||||||
|
|
||||||
|
(define trace-sub? (make-parameter #f))
|
||||||
|
|
||||||
;; Type Type -> Bool
|
;; Type Type -> Bool
|
||||||
;; subtyping
|
;; subtyping
|
||||||
(define (<: t1 t2)
|
(define (<: t1 t2)
|
||||||
|
(when (trace-sub?)
|
||||||
|
(printf "~a\n<:\n~a\n" t1 t2))
|
||||||
(syntax-parse #`(#,t1 #,t2)
|
(syntax-parse #`(#,t1 #,t2)
|
||||||
[(_ ~★/t)
|
[(_ ~★/t)
|
||||||
(flat-type? t1)]
|
(flat-type? t1)]
|
||||||
|
@ -749,10 +798,21 @@
|
||||||
[((~Actor τ1) (~Actor τ2))
|
[((~Actor τ1) (~Actor τ2))
|
||||||
(and (<: #'τ1 #'τ2)
|
(and (<: #'τ1 #'τ2)
|
||||||
(<: (∩ (strip-? #'τ1) #'τ2) #'τ1))]
|
(<: (∩ (strip-? #'τ1) #'τ2) #'τ1))]
|
||||||
[((~→fn τ-in1 ... τ-out1) (~→fn τ-in2 ... τ-out2))
|
[((~proc τ-in1 ... -> τ-out1 #:spawns (~seq S1 ...)
|
||||||
|
#:roles (~seq R1 ...)
|
||||||
|
#:endpoints (~seq E1 ...))
|
||||||
|
(~proc τ-in2 ... -> τ-out2 #:spawns (~seq S2 ...)
|
||||||
|
#:roles (~seq R2 ...)
|
||||||
|
#:endpoints (~seq E2 ...)))
|
||||||
(and (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...))
|
(and (stx-length=? #'(τ-in1 ...) #'(τ-in2 ...))
|
||||||
(stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...))
|
(stx-andmap <: #'(τ-in2 ...) #'(τ-in1 ...))
|
||||||
(<: #'τ-out1 #'τ-out2))]
|
(<: #'τ-out1 #'τ-out2)
|
||||||
|
(<: (mk-Actor- (list (mk-U*- #'(S1 ...))))
|
||||||
|
(mk-Actor- (list (mk-U*- #'(S2 ...)))))
|
||||||
|
(<: (mk-U*- #'(R1 ...))
|
||||||
|
(mk-U*- #'(R2 ...)))
|
||||||
|
(<: (mk-U*- #'(E1 ...))
|
||||||
|
(mk-U*- #'(E2 ...))))]
|
||||||
[(~Discard _)
|
[(~Discard _)
|
||||||
#t]
|
#t]
|
||||||
[(X:id Y:id)
|
[(X:id Y:id)
|
||||||
|
@ -763,6 +823,10 @@
|
||||||
(<: #'τ1 #'τ2-X/Y)]
|
(<: #'τ1 #'τ2-X/Y)]
|
||||||
[((~Base τ1:id) (~Base τ2:id))
|
[((~Base τ1:id) (~Base τ2:id))
|
||||||
(free-identifier=? #'τ1 #'τ2)]
|
(free-identifier=? #'τ1 #'τ2)]
|
||||||
|
[((~Role (x) _ ...) (~Role (y) _ ...))
|
||||||
|
;; Extremely Coarse subtyping for Role types
|
||||||
|
(type=? t1 t2)]
|
||||||
|
;; TODO: clauses for Roles, effectful functions, and so on
|
||||||
[((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...))
|
[((~Any/bvs τ-cons1 () τ1 ...) (~Any/bvs τ-cons2 () τ2 ...))
|
||||||
#:when (free-identifier=? #'τ-cons1 #'τ-cons2)
|
#:when (free-identifier=? #'τ-cons1 #'τ-cons2)
|
||||||
#:do [(define variances (syntax-property #'τ-cons1 'arg-variances))]
|
#:do [(define variances (syntax-property #'τ-cons1 'arg-variances))]
|
||||||
|
@ -781,7 +845,6 @@
|
||||||
(<: ty2 ty1))]
|
(<: ty2 ty1))]
|
||||||
[(== irrelevant)
|
[(== irrelevant)
|
||||||
#t]))]
|
#t]))]
|
||||||
;; TODO: clauses for Roles, effectful functions, and so on
|
|
||||||
[_
|
[_
|
||||||
#f]))
|
#f]))
|
||||||
|
|
||||||
|
@ -886,7 +949,7 @@
|
||||||
[X:id
|
[X:id
|
||||||
#t]
|
#t]
|
||||||
[(~Base _) #t]
|
[(~Base _) #t]
|
||||||
[(~Any/bvs τ-cons () τ ...)
|
[(~Any/bvs τ-cons (X ...) τ ...)
|
||||||
(stx-andmap finite? #'(τ ...))]))
|
(stx-andmap finite? #'(τ ...))]))
|
||||||
|
|
||||||
;; PatternType -> Type
|
;; PatternType -> Type
|
||||||
|
@ -1019,19 +1082,53 @@
|
||||||
|
|
||||||
(define-typed-syntax inst
|
(define-typed-syntax inst
|
||||||
[(_ e τ:type ...) ≫
|
[(_ e τ:type ...) ≫
|
||||||
#:fail-unless (stx-andmap instantiable? #'(τ.norm ...))
|
#:cut
|
||||||
"types must be instantiable"
|
|
||||||
[⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
|
[⊢ e ≫ e- ⇒ (~∀ tvs τ_body)]
|
||||||
|
#:fail-unless (stx-andmap instantiable? #'(τ.norm ...) #'tvs)
|
||||||
|
"types must be instantiable"
|
||||||
#:fail-unless (pure? #'e-) "expression must be pure"
|
#:fail-unless (pure? #'e-) "expression must be pure"
|
||||||
--------
|
--------
|
||||||
[⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]]
|
[⊢ e- ⇒ #,(substs #'(τ.norm ...) #'tvs #'τ_body)]]
|
||||||
[(_ e) ≫ --- [≻ e]])
|
[(_ e) ≫ --- [≻ e]])
|
||||||
|
|
||||||
;; Type -> Bool
|
;; Identifier Type -> Bool
|
||||||
;; determine if a type is suitable for instantiating a variable
|
;; determine if a type is suitable for instantiating a variable
|
||||||
(define-for-syntax (instantiable? ty)
|
;; only row variables may be instantiated with effectful/higher-order types
|
||||||
(and (flat-type? ty)
|
(define-for-syntax (instantiable? x ty)
|
||||||
(finite? ty)))
|
(or (row-variable? x)
|
||||||
|
(and (flat-type? ty)
|
||||||
|
(finite? ty))))
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
;; CONVENTION: Type variables for effects are prefixed with ρ
|
||||||
|
(define (row-variable? x)
|
||||||
|
(and (identifier? x)
|
||||||
|
(char=? (string-ref (symbol->string (syntax-e x)) 0) #\ρ)))
|
||||||
|
|
||||||
|
(define-syntax-class row-id
|
||||||
|
#:attributes ()
|
||||||
|
(pattern x:id #:when (row-variable? #'x))))
|
||||||
|
|
||||||
|
;; instantiate row variables with types from procedure arguments
|
||||||
|
;; BRITTLE?
|
||||||
|
(define-typed-syntax (call/inst e:expr args:expr ...) ≫
|
||||||
|
[⊢ e ≫ e- (⇒ : (~∀ (X:row-id ...) τ))]
|
||||||
|
[⊢ args ≫ args- (⇒ : τ-a)] ...
|
||||||
|
#:fail-unless (all-pure? #'(e- args- ...))
|
||||||
|
"expressions must be pure"
|
||||||
|
;; ordering pretty arbitrary
|
||||||
|
#:with ((~or (~proc _ ... -> _
|
||||||
|
#:spawns (~seq S ...)
|
||||||
|
#:roles (~seq R ...)
|
||||||
|
#:endpoints (~seq E ...))
|
||||||
|
_) ...) #'(τ-a ...)
|
||||||
|
#:with (SS ...) (if (attribute S) #'(S ... ...) #'())
|
||||||
|
#:with (RR ...) (if (attribute R) #'(R ... ...) #'())
|
||||||
|
#:with (EE ...) (if (attribute E) #'(E ... ...) #'())
|
||||||
|
#:fail-unless (stx-length=? #'(X ...) #'(SS ... RR ... EE ...))
|
||||||
|
"found the wrong number of effects"
|
||||||
|
-------------------------------------------------------
|
||||||
|
[≻ ((inst e- SS ... RR ... EE ...) args- ...)])
|
||||||
|
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
;; Sequencing & Definitions
|
;; Sequencing & Definitions
|
||||||
|
@ -1214,6 +1311,11 @@
|
||||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||||
|
|
||||||
(define-typed-syntax #%app
|
(define-typed-syntax #%app
|
||||||
|
;; Polymorphic, Effectful Function - Perform Simple Matching on Argument Types
|
||||||
|
[(_ e_fn e_arg ...) ≫
|
||||||
|
[⊢ e_fn ≫ e_fn- (⇒ : (~∀ (X:row-id ...+) τ))]
|
||||||
|
---------------------------------------------
|
||||||
|
[≻ (call/inst e_fn- e_arg ...)]]
|
||||||
;; Polymorphic, Pure Function - Perform Local Inference
|
;; Polymorphic, Pure Function - Perform Local Inference
|
||||||
[(_ e_fn e_arg ...) ≫
|
[(_ e_fn e_arg ...) ≫
|
||||||
;; compute fn type (ie ∀ and →)
|
;; compute fn type (ie ∀ and →)
|
||||||
|
@ -1225,8 +1327,9 @@
|
||||||
#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
|
#:with [[e_arg- ...] Xs* cs] (solve #'Xs #'tyX_args this-syntax)
|
||||||
;; make sure types are legal
|
;; make sure types are legal
|
||||||
#:with tyXs (inst-types/cs #'Xs* #'cs #'Xs)
|
#:with tyXs (inst-types/cs #'Xs* #'cs #'Xs)
|
||||||
#:fail-unless (for/and ([ty (in-syntax #'tyXs)])
|
#:fail-unless (for/and ([ty (in-syntax #'tyXs)]
|
||||||
(instantiable? ty))
|
[x (in-syntax #'Xs)])
|
||||||
|
(instantiable? x ty))
|
||||||
"type variables must be flat and finite"
|
"type variables must be flat and finite"
|
||||||
;; instantiate polymorphic function type
|
;; instantiate polymorphic function type
|
||||||
#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
|
#:with [τ_in ... τ_out] (inst-types/cs #'Xs* #'cs #'tyX_args)
|
||||||
|
@ -1263,7 +1366,7 @@
|
||||||
(~Spawns τ-s ...))))]
|
(~Spawns τ-s ...))))]
|
||||||
#:fail-unless (pure? #'e_fn-) "expression not allowed to have effects"
|
#:fail-unless (pure? #'e_fn-) "expression not allowed to have effects"
|
||||||
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
|
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
|
||||||
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
|
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
|
||||||
[⊢ e_arg ≫ e_arg- (⇐ : τ_in)] ...
|
[⊢ e_arg ≫ e_arg- (⇐ : τ_in)] ...
|
||||||
#:fail-unless (stx-andmap pure? #'(e_arg- ...)) "expressions not allowed to have effects"
|
#:fail-unless (stx-andmap pure? #'(e_arg- ...)) "expressions not allowed to have effects"
|
||||||
------------------------------------------------------------------------
|
------------------------------------------------------------------------
|
||||||
|
|
|
@ -13,7 +13,7 @@
|
||||||
FacetName Field ★/t
|
FacetName Field ★/t
|
||||||
Observe Inbound Outbound Actor U ⊥
|
Observe Inbound Outbound Actor U ⊥
|
||||||
Computation Value Endpoints Roles Spawns
|
Computation Value Endpoints Roles Spawns
|
||||||
→fn
|
→fn proc
|
||||||
;; Statements
|
;; Statements
|
||||||
let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
|
let let* if spawn dataspace start-facet set! begin stop begin/dataflow #;unsafe-do
|
||||||
when unless send! define
|
when unless send! define
|
||||||
|
@ -27,7 +27,7 @@
|
||||||
assert on field
|
assert on field
|
||||||
;; expressions
|
;; expressions
|
||||||
tuple select lambda ref observe inbound outbound
|
tuple select lambda ref observe inbound outbound
|
||||||
Λ inst
|
Λ inst call/inst
|
||||||
;; making types
|
;; making types
|
||||||
define-type-alias
|
define-type-alias
|
||||||
assertion-struct
|
assertion-struct
|
||||||
|
|
|
@ -0,0 +1,17 @@
|
||||||
|
#lang typed/syndicate/roles
|
||||||
|
|
||||||
|
(require rackunit/turnstile)
|
||||||
|
|
||||||
|
(define (∀ (ρ) (assert-something! [p : (proc → ★/t #:endpoints (ρ))]))
|
||||||
|
(p))
|
||||||
|
|
||||||
|
(define (test-fun)
|
||||||
|
(call/inst assert-something! (lambda () (assert 5))))
|
||||||
|
|
||||||
|
|
||||||
|
(check-type test-fun : (proc → ★/t #:endpoints ((Shares Int))))
|
||||||
|
|
||||||
|
(define (test-call/inst-insertion)
|
||||||
|
(assert-something! (lambda () (assert 5))))
|
||||||
|
|
||||||
|
(check-type test-call/inst-insertion : (proc → ★/t #:endpoints ((Shares Int))))
|
Loading…
Reference in New Issue