commit 362b0f310d9dddfa4cd562a9d08c692a87c401a6
parent e8faad889b4fdd8a80fed1dd888e549d0b3b60c7
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Mon, 3 Oct 2016 14:28:15 -0400
manually merge mlish.rkt from adhoc branch to mlish+adhoc.rkt
Diffstat:
11 files changed, 4391 insertions(+), 7 deletions(-)
diff --git a/macrotypes/examples/mlish+adhoc.rkt b/macrotypes/examples/mlish+adhoc.rkt
@@ -0,0 +1,1718 @@
+#lang s-exp "../typecheck.rkt"
+(require racket/fixnum racket/flonum)
+
+(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let let* and #%datum begin
+ #:rename [~→ ~ext-stlc:→])
+;(reuse [inst sysf:inst] #:from "sysf.rkt")
+(require (rename-in (only-in "sysf.rkt" inst) [inst sysf:inst]))
+(provide inst)
+(require (only-in "ext-stlc.rkt" →?))
+(require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
+(reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
+(require (only-in "stlc+rec-iso.rkt" ~× ×?)) ; using current-type=? from here
+(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
+(reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
+(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))
+(require (only-in "stlc+cons.rkt" ~List List? List))
+(provide List)
+(reuse ref deref := Ref #:from "stlc+box.rkt")
+(require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×)
+ [tup rec] [proj get] [× ××]))
+(provide rec get ××)
+;; for pattern matching
+(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list)))
+(require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup)))
+
+(provide → →/test =>/test match2 define-type)
+
+(provide define-typeclass define-instance)
+
+;; ML-like language + ad-hoc polymorphism
+;; - top level recursive functions
+;; - user-definable algebraic datatypes
+;; - pattern matching
+;; - (local) type inference
+;;
+;; - type classes
+
+(define-type-constructor => #:arity > 0)
+
+;; type class helper fns
+(begin-for-syntax
+ (define (mk-app-err-msg stx #:expected [expected-τs #'()]
+ #:given [given-τs #'()]
+ #:note [note ""]
+ #:name [name #f]
+ #:action [other #f])
+ (syntax-parse stx
+ #;[(app . rst)
+ #:when (not (equal? '#%app (syntax->datum #'app)))
+ (mk-app-err-msg (syntax/loc stx (#%app app . rst))
+ #:expected expected-τs
+ #:given given-τs
+ #:note note
+ #:name name)]
+ [(app e_fn e_arg ...)
+ (define fn-name
+ (if name name
+ (format "function ~a"
+ (syntax->datum (or (get-orig #'e_fn) #'e_fn)))))
+ (define action (if other other "applying"))
+ (string-append
+ (format "~a (~a:~a):\nType error "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx))
+ action " "
+ fn-name ". " note "\n"
+ (format " Expected: ~a argument(s) with type(s): " (stx-length expected-τs))
+ (types->str expected-τs) "\n"
+ " Given:\n"
+ (string-join
+ (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
+ (syntax->datum #'(e_arg ...))
+ (if (stx-length=? #'(e_arg ...) given-τs)
+ (stx-map type->str given-τs)
+ (stx-map (lambda (e) "?") #'(e_arg ...))))
+ "\n")
+ "\n")]))
+ (define (type-hash-code tys) ; tys should be fully expanded
+ (equal-hash-code (syntax->datum (if (syntax? tys) tys #`#,tys))))
+ (define (mangle o tys)
+ (format-id o "~a~a" o (type-hash-code tys)))
+ ;; pattern expander for type class
+ (define-syntax ~TC
+ (pattern-expander
+ (syntax-parser
+ [(_ [generic-op ty-concrete-op] (~and ooo (~literal ...)))
+ #'(_ (_ (_ generic-op) ty-concrete-op) ooo)]
+ [(_ . ops+tys)
+ #:with expanded (generate-temporary)
+ #'(~and expanded
+ (~parse (_ (_ (_ gen-op) ty-op) (... ...))
+ #'expanded)
+ (~parse ops+tys #'((gen-op ty-op) (... ...))))])))
+ (define-syntax ~TC-base
+ (pattern-expander
+ (syntax-parser
+ [(_ . pat)
+ #:with expanded (generate-temporary)
+ #'(~and expanded
+ (~parse ((~TC . pat) . _) (flatten-TC #'expanded)))])))
+ (define-syntax ~TCs
+ (pattern-expander
+ (syntax-parser
+ ;; pat should be of shape ([op ty] ...)
+ [(_ pat (~and ooo (~literal ...)))
+ #:with expanded (generate-temporary)
+ ;; (stx-map (compose remove-dups flatten-TC) #'expanded)
+ ;; produces [List [List [List op+ty]]]
+ ;; - inner [List op+ty] is from the def of a TC
+ ;; - second List is from the flattened subclass TCs
+ ;; - outer List is bc this pattern matces multiple TCs
+ ;; This pattern expander collapses the inner two Lists
+ #'(~and expanded
+ (~parse (((~TC [op ty] (... ...)) (... ...)) ooo)
+ (stx-map (compose remove-dups flatten-TC) #'expanded))
+ (~parse (pat ooo) #'(([op ty] (... ...) (... ...)) ooo)))])))
+ (define (flatten-TC TC)
+ (syntax-parse TC
+ [(~=> sub-TC ... base-TC)
+ (cons #'base-TC (stx-appendmap flatten-TC #'(sub-TC ...)))]))
+ (define (remove-dups TCs)
+ (syntax-parse TCs
+ [() #'()]
+ [(TC . rst)
+ (cons #'TC (stx-filter (lambda (s) (not (typecheck? s #'TC))) (remove-dups #'rst)))])))
+;; type inference constraint solving
+(begin-for-syntax
+ ;; matching possibly polymorphic types
+ (define-syntax ~?∀
+ (pattern-expander
+ (lambda (stx)
+ (syntax-case stx ()
+ [(?∀ vars-pat body-pat)
+ #'(~or (~∀ vars-pat body-pat)
+ (~and (~not (~∀ _ _))
+ (~parse vars-pat #'())
+ body-pat))]))))
+
+ ;; type inference constraint solving
+ (define (compute-constraint τ1-τ2)
+ (syntax-parse τ1-τ2
+ [(X:id τ) #'((X τ))]
+ [((~Any tycons1 τ1 ...) (~Any tycons2 τ2 ...))
+ #:when (typecheck? #'tycons1 #'tycons2)
+ (compute-constraints #'((τ1 τ2) ...))]
+ ; should only be monomorphic?
+ [((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
+ (compute-constraints #'((τ1 τ2) ...))]
+ [_ #'()]))
+ (define (compute-constraints τs)
+ (stx-appendmap compute-constraint τs))
+
+ (define (solve-constraint x-τ)
+ (syntax-parse x-τ
+ [(X:id τ) #'((X τ))]
+ [_ #'()]))
+ (define (solve-constraints cs)
+ (stx-appendmap compute-constraint cs))
+
+ (define (lookup x substs)
+ (syntax-parse substs
+ [((y:id τ) . rst)
+ #:when (free-identifier=? #'y x)
+ #'τ]
+ [(_ . rst) (lookup x #'rst)]
+ [() #f]))
+
+ ;; find-unsolved-Xs : (Stx-Listof Id) Constraints -> (Listof Id)
+ ;; finds the free Xs that aren't constrained by cs
+ (define (find-unsolved-Xs Xs cs)
+ (for/list ([X (in-list (stx->list Xs))]
+ #:when (not (lookup X cs)))
+ X))
+
+ ;; lookup-Xs/keep-unsolved : (Stx-Listof Id) Constraints -> (Listof Type-Stx)
+ ;; looks up each X in the constraints, returning the X if it's unconstrained
+ (define (lookup-Xs/keep-unsolved Xs cs)
+ (for/list ([X (in-list (stx->list Xs))])
+ (or (lookup X cs) X)))
+
+ ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args
+ ;; stx = the application stx = (#%app e_fn e_arg ...)
+ ;; tyXs = input and output types from fn type
+ ;; ie (typeof e_fn) = (-> . tyXs)
+ ;; It infers the types of arguments from left-to-right,
+ ;; and it short circuits if it's done early.
+ ;; It returns list of 3 values if successful, else throws a type error
+ ;; - a list of the arguments that it expanded
+ ;; - a list of the the un-constrained type variables
+ ;; - the constraints for substituting the types
+ (define (solve Xs tyXs stx)
+ (syntax-parse tyXs
+ [(τ_inX ... τ_outX)
+ ;; generate initial constraints with expected type and τ_outX
+ #:with expected-ty (get-expected-type stx)
+ (define initial-cs
+ (if (syntax-e #'expected-ty)
+ (compute-constraint (list #'τ_outX ((current-type-eval) #'expected-ty)))
+ #'()))
+ (syntax-parse stx
+ [(_ e_fn . args)
+ (define-values (as- cs)
+ (for/fold ([as- null] [cs initial-cs])
+ ([a (in-list (syntax->list #'args))]
+ [tyXin (in-list (syntax->list #'(τ_inX ...)))]
+ #:break (empty? (find-unsolved-Xs Xs cs)))
+ (define/with-syntax [a- ty_a] (infer+erase a))
+ (values
+ (cons #'a- as-)
+ (stx-append cs (compute-constraint (list tyXin #'ty_a))))))
+
+ (list (reverse as-) (find-unsolved-Xs Xs cs) cs)])]))
+
+ (define (raise-app-poly-infer-error stx expected-tys given-tys e_fn)
+ (type-error #:src stx
+ #:msg (mk-app-err-msg stx #:expected expected-tys #:given given-tys
+ #:note (format "Could not infer instantiation of polymorphic function ~a."
+ (syntax->datum (get-orig e_fn))))))
+
+ ;; instantiate polymorphic types
+ ;; inst-type : (Listof Type) (Listof Id) Type -> Type
+ ;; Instantiates ty with the tys-solved substituted for the Xs, where the ith
+ ;; identifier in Xs is associated with the ith type in tys-solved
+ (define (inst-type tys-solved Xs ty)
+ (substs tys-solved Xs ty))
+
+ ;; inst-type/cs : (Stx-Listof Id) Constraints Type-Stx -> Type-Stx
+ ;; Instantiates ty, substituting each identifier in Xs with its mapping in cs.
+ (define (inst-type/cs Xs cs ty)
+ (define tys-solved (lookup-Xs/keep-unsolved Xs cs))
+ (inst-type tys-solved Xs ty))
+ ;; inst-types/cs : (Stx-Listof Id) Constraints (Stx-Listof Type-Stx) -> (Listof Type-Stx)
+ ;; the plural version of inst-type/cs
+ (define (inst-types/cs Xs cs tys)
+ (stx-map (lambda (t) (inst-type/cs Xs cs t)) tys))
+
+ ;; compute unbound tyvars in one unexpanded type ty
+ (define (compute-tyvar1 ty)
+ (syntax-parse ty
+ [X:id #'(X)]
+ [() #'()]
+ [(C t ...) (stx-appendmap compute-tyvar1 #'(t ...))]))
+ ;; computes unbound ids in (unexpanded) tys, to be used as tyvars
+ (define (compute-tyvars tys)
+ (define Xs (stx-appendmap compute-tyvar1 tys))
+ (filter
+ (lambda (X)
+ (with-handlers
+ ([exn:fail:syntax:unbound? (lambda (e) #t)]
+ [exn:fail:type:infer? (lambda (e) #t)])
+ (let ([X+ ((current-type-eval) X)])
+ (not (or (tyvar? X+) (type? X+))))))
+ (stx-remove-dups Xs))))
+
+;; define --------------------------------------------------
+;; for function defs, define infers type variables
+;; - since the order of the inferred type variables depends on expansion order,
+;; which is not known to programmers, to make the result slightly more
+;; intuitive, we arbitrarily sort the inferred tyvars lexicographically
+(define-typed-syntax define/tc #:export-as define
+ [(_ x:id e)
+ #:with (e- τ) (infer+erase #'e)
+ #:with y (generate-temporary)
+ #'(begin-
+ (define-syntax- x (make-rename-transformer (⊢ y : τ)))
+ (define- y e-))]
+ ; explicit "forall"
+ [(_ Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e)
+ #:when (brace? #'Ys)
+ ;; TODO; remove this code duplication
+ #:with g (add-orig (generate-temporary #'f) #'f)
+ #:with e_ann (syntax/loc #'e (add-expected e τ_out))
+ #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
+ ;; TODO: check that specified return type is correct
+ ;; - currently cannot do it here; to do the check here, need all types of
+ ;; top-lvl fns, since they can call each other
+ #:with (~and ty_fn_expected (~∀ _ (~ext-stlc:→ _ ... out_expected)))
+ ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...)))
+ #`(begin-
+ (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ (define- g
+ (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]
+ ;; alternate type sig syntax, after parameter names
+ [(_ (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b)
+ (syntax/loc stx (define/tc (f [x : ty] ... -> ty_out) . b))]
+ [(_ (f:id [x:id (~datum :) τ] ... ; no TC
+ (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e)
+ #:with (~and Ys (Y ...)) (compute-tyvars #'(τ ... τ_out))
+ #:with g (add-orig (generate-temporary #'f) #'f)
+ #:with e_ann (syntax/loc #'e (add-expected e τ_out)) ; must be macro bc t_out may have unbound tvs
+ #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
+ ;; TODO: check that specified return type is correct
+ ;; - currently cannot do it here; to do the check here, need all types of
+ ;; top-lvl fns, since they can call each other
+ #:with ty_fn_expected
+ (set-stx-prop/preserved
+ ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...)))
+ 'orig
+ (list #'(→ τ+orig ...)))
+ #`(begin-
+ (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ (define- g
+ (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]
+ [(_ (f:id [x:id (~datum :) τ] ...
+ (~seq #:where TC ...)
+ (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e)
+ #:with (~and Ys (Y ...)) (compute-tyvars #'(τ ... τ_out))
+ #:with g (add-orig (generate-temporary #'f) #'f)
+ #:with e_ann (syntax/loc #'e (add-expected e τ_out)) ; must be macro bc t_out may have unbound tvs
+ #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
+ ;; TODO: check that specified return type is correct
+ ;; - currently cannot do it here; to do the check here, need all types of
+ ;; top-lvl fns, since they can call each other
+ #:with (~and ty_fn_expected (~∀ _ (~=> _ ... (~ext-stlc:→ _ ... out_expected))))
+ (syntax-property
+ ((current-type-eval) #'(∀ Ys (=> TC ... (ext-stlc:→ τ+orig ...))))
+ 'orig
+ (list #'(→ τ+orig ...)))
+ #`(begin-
+ (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ #,(quasisyntax/loc stx
+ (define- g
+ ;(Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
+ (liftedλ {Y ...} ([x : τ] ... #:where TC ...)
+ #,(syntax/loc #'e_ann (ext-stlc:begin e_body ... e_ann))))))])
+
+;; define-type -----------------------------------------------
+;; TODO: should validate τ as part of define-type definition (before it's used)
+;; - not completely possible, since some constructors may not be defined yet,
+;; ie, mutually recursive datatypes
+;; for now, validate types but punt if encountering unbound ids
+(define-syntax (define-type stx)
+ (syntax-parse stx
+ [(_ Name:id . rst)
+ #:with NewName (generate-temporary #'Name)
+ #:with Name2 (add-orig #'(NewName) #'Name)
+ #`(begin-
+ (define-type Name2 . #,(subst #'Name2 #'Name #'rst))
+ (stlc+rec-iso:define-type-alias Name Name2))]
+ [(_ (Name:id X:id ...)
+ ;; constructors must have the form (Cons τ ...)
+ ;; but the first ~or clause accepts 0-arg constructors as ids;
+ ;; the ~and is a workaround to bind the duplicate Cons ids (see Ryan's email)
+ (~and (~or (~and IdCons:id
+ (~parse (Cons [fld (~datum :) τ] ...) #'(IdCons)))
+ (Cons [fld (~datum :) τ] ...)
+ (~and (Cons τ ...)
+ (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
+ ;; validate tys
+ #:with (ty_flat ...) (stx-flatten #'((τ ...) ...))
+ #:with (_ _ (_ _ (_ _ (_ _ ty+ ...))))
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (λ (e)
+ (define X (stx-car (exn:fail:syntax-exprs e)))
+ #`(lambda () (let-syntax () (let-syntax () (#%app void unbound)))))])
+ (expand/df
+ #`(lambda (X ...)
+ (let-syntax
+ ([Name
+ (syntax-parser
+ [(_ X ...) (mk-type #'void)]
+ [stx
+ (type-error
+ #:src #'stx
+ #:msg
+ (format "Improper use of constructor ~a; expected ~a args, got ~a"
+ (syntax->datum #'Name) (stx-length #'(X ...))
+ (stx-length (stx-cdr #'stx))))])]
+ [X (make-rename-transformer (⊢ X #%type))] ...)
+ (void ty_flat ...)))))
+ #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
+ (stx-map
+ (lambda (t+ t) (unless (type? t+)
+ (type-error #:src t
+ #:msg "~a is not a valid type" t)))
+ #'(ty+ ...) #'(ty_flat ...)))
+ #:with NameExpander (format-id #'Name "~~~a" #'Name)
+ #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name)
+ #:with (StructName ...) (generate-temporaries #'(Cons ...))
+ #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((exposed-acc ...) ...)
+ (stx-map
+ (λ (C fs) (stx-map (λ (f) (format-id C "~a-~a" C f)) fs))
+ #'(Cons ...) #'((fld ...) ...))
+ #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
+ #'(StructName ...) #'((fld ...) ...))
+ #:with (Cons? ...) (stx-map mk-? #'(StructName ...))
+ #:with (exposed-Cons? ...) (stx-map mk-? #'(Cons ...))
+ #`(begin-
+ (define-syntax- (NameExtraInfo stx)
+ (syntax-parse stx
+ [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)]))
+ (define-type-constructor Name
+ #:arity = #,(stx-length #'(X ...))
+ #:extra-info 'NameExtraInfo
+ #:no-provide)
+ (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
+ (define-syntax- (exposed-acc stx) ; accessor for records
+ (syntax-parse stx
+ [_:id (⊢ acc (∀ (X ...) (ext-stlc:→ (Name X ...) τ)))]
+ [(o . rst) ; handle if used in fn position
+ #:with app (datum->syntax #'o '#%app)
+ #`(app
+ #,(assign-type #'acc #'(∀ (X ...) (ext-stlc:→ (Name X ...) τ)))
+ . rst)])) ... ...
+ (define-syntax- (exposed-Cons? stx) ; predicates for each variant
+ (syntax-parse stx
+ [_:id (⊢ Cons? (∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))]
+ [(o . rst) ; handle if used in fn position
+ #:with app (datum->syntax #'o '#%app)
+ #`(app
+ #,(assign-type #'Cons? #'(∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))
+ . rst)])) ...
+ (define-syntax- (Cons stx)
+ (syntax-parse stx
+ ; no args and not polymorphic
+ [C:id #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) #'(C)]
+ ; no args but polymorphic, check inferred type
+ [C:id
+ #:when (stx-null? #'(τ ...))
+ #:with τ-expected (syntax-property #'C 'expected-type)
+ #:fail-unless (syntax-e #'τ-expected)
+ (raise
+ (exn:fail:type:infer
+ (string-append
+ (format "TYPE-ERROR: ~a (~a:~a): "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx))
+ (format "cannot infer type of ~a; add annotations"
+ (syntax->datum #'C)))
+ (current-continuation-marks)))
+ #:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected)
+ #'(C {τ-expected-arg (... ...)})]
+ [_:id (⊢ StructName (∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))] ; HO fn
+ [(C τs e_arg ...)
+ #:when (brace? #'τs) ; commit to this clause
+ #:with {~! τ_X:type (... ...)} #'τs
+ #:with (τ_in:type (... ...)) ; instantiated types
+ (stx-map
+ (λ (t) (substs #'(τ_X.norm (... ...)) #'(X ...) t))
+ #'(τ ...))
+ #:with ([e_arg- τ_arg] ...)
+ (stx-map
+ (λ (e τ_e)
+ (infer+erase (set-stx-prop/preserved e 'expected-type τ_e)))
+ #'(e_arg ...) #'(τ_in.norm (... ...)))
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
+ (mk-app-err-msg (syntax/loc stx (#%app C e_arg ...))
+ #:expected #'(τ_in.norm (... ...)) #:given #'(τ_arg ...)
+ #:name (format "constructor ~a" 'Cons))
+ (⊢ (StructName e_arg- ...) : (Name τ_X (... ...)))]
+ [(C . args) ; no type annotations, must infer instantiation
+ #:with StructName/ty
+ (set-stx-prop/preserved
+ (⊢ StructName : (∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))
+ 'orig
+ (list #'C))
+ ; stx/loc transfers expected-type
+ (syntax/loc stx (mlish:#%app StructName/ty . args))]))
+ ...)]))
+
+;; match --------------------------------------------------
+(begin-for-syntax
+ (define (get-ctx pat ty)
+ (unify-pat+ty (list pat ty)))
+ (define (unify-pat+ty pat+ty)
+ (syntax-parse pat+ty
+ [(pat ty) #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
+ (syntax-parse #'pat
+ [{(~datum _)} #'()]
+ [{(~literal stlc+cons:nil)} #'()]
+ [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
+ #:when (get-extra-info #'ty)
+ #'()]
+ ;; comma tup syntax always has parens
+ [{(~and ps (p1 (unq p) ...))}
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ (unify-pat+ty #'(ps ty))]
+ [{p ...}
+ (unify-pat+ty #'((p ...) ty))])] ; pair
+ [((~datum _) ty) #'()]
+ [((~or (~literal stlc+cons:nil)) ty) #'()]
+ [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens)
+ #:with (_ (_ (_ C) . _) ...) (get-extra-info #'ty)
+ #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
+ #'()]
+ [(x:id ty) #'((x ty))]
+ [((p1 (unq p) ...) ty) ; comma tup stx
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ #:with (~× t ...) #'ty
+ #:with (pp ...) #'(p1 p ...)
+ (unifys #'([pp t] ...))]
+ [(((~literal stlc+tup:tup) p ...) ty) ; tup
+ #:with (~× t ...) #'ty
+ (unifys #'([p t] ...))]
+ [(((~literal stlc+cons:list) p ...) ty) ; known length list
+ #:with (~List t) #'ty
+ (unifys #'([p t] ...))]
+ [(((~seq p (~datum ::)) ... rst) ty) ; nicer cons stx
+ #:with (~List t) #'ty
+ (unifys #'([p t] ... [rst ty]))]
+ [(((~literal stlc+cons:cons) p ps) ty) ; arb length list
+ #:with (~List t) #'ty
+ (unifys #'([p t] [ps ty]))]
+ [((Name p ...) ty)
+ #:with (_ (_ Cons) _ _ [_ _ τ] ...)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst)
+ (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+ (stx-cdr (get-extra-info #'ty)))
+ (unifys #'([p τ] ...))]
+ [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t))
+ #'()]))
+ (define (unifys p+tys) (stx-appendmap unify-pat+ty p+tys))
+
+ (define (compile-pat p ty)
+ (syntax-parse p
+ [pat #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
+ (syntax-parse #'pat
+ [{(~datum _)} #'_]
+ [{(~literal stlc+cons:nil)} (syntax/loc p (list))]
+ [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
+ #:when (get-extra-info ty)
+ (compile-pat #'(A) ty)]
+ ;; comma tup stx always has parens
+ [{(~and ps (p1 (unq p) ...))}
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ (compile-pat #'ps ty)]
+ [{pat ...} (compile-pat (syntax/loc p (pat ...)) ty)])]
+ [(~datum _) #'_]
+ [(~literal stlc+cons:nil) ; nil
+ #'(list)]
+ [A:id ; disambiguate 0-arity constructors (that don't need parens)
+ #:with (_ (_ (_ C) . _) ...) (get-extra-info ty)
+ #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
+ (compile-pat #'(A) ty)]
+ [x:id p]
+ [(p1 (unq p) ...) ; comma tup stx
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ #:with (~× t ...) ty
+ #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'(p1 p ...) #'(t ...))
+ #'(list p- ...)]
+ [((~literal stlc+tup:tup) . pats)
+ #:with (~× . tys) ty
+ #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'pats #'tys)
+ (syntax/loc p (list p- ...))]
+ [((~literal stlc+cons:list) . ps)
+ #:with (~List t) ty
+ #:with (p- ...) (stx-map (lambda (p) (compile-pat p #'t)) #'ps)
+ (syntax/loc p (list p- ...))]
+ [((~seq pat (~datum ::)) ... last) ; nicer cons stx
+ #:with (~List t) ty
+ #:with (p- ...) (stx-map (lambda (pp) (compile-pat pp #'t)) #'(pat ...))
+ #:with last- (compile-pat #'last ty)
+ (syntax/loc p (list-rest p- ... last-))]
+ [((~literal stlc+cons:cons) p ps)
+ #:with (~List t) ty
+ #:with p- (compile-pat #'p #'t)
+ #:with ps- (compile-pat #'ps ty)
+ #'(cons p- ps-)]
+ [(Name . pats)
+ #:with (_ (_ Cons) (_ StructName) _ [_ _ τ] ...)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst)
+ (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+ (stx-cdr (get-extra-info ty)))
+ #:with (p- ...) (stx-map compile-pat #'pats #'(τ ...))
+ (syntax/loc p (StructName p- ...))]))
+
+ ;; pats = compiled pats = racket pats
+ (define (check-exhaust pats ty)
+ (define (else-pat? p)
+ (syntax-parse p [(~literal _) #t] [_ #f]))
+ (define (nil-pat? p)
+ (syntax-parse p
+ [((~literal list)) #t]
+ [_ #f]))
+ (define (non-nil-pat? p)
+ (syntax-parse p
+ [((~literal list-rest) . rst) #t]
+ [((~literal cons) . rst) #t]
+ [_ #f]))
+ (define (tup-pat? p)
+ (syntax-parse p
+ [((~literal list) . _) #t] [_ #f]))
+ (cond
+ [(or (stx-ormap else-pat? pats) (stx-ormap identifier? pats)) #t]
+ [(List? ty) ; lists
+ (unless (stx-ormap nil-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing nil clause for list expression"
+ (syntax-line last) (syntax-column last)))))
+ (unless (stx-ormap non-nil-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing clause for non-empty, arbitrary length list"
+ (syntax-line last) (syntax-column last)))))
+ #t]
+ [(×? ty) ; tuples
+ (unless (stx-ormap tup-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing pattern for tuple expression"
+ (syntax-line last) (syntax-column last)))))
+ (syntax-parse pats
+ [((_ p ...) ...)
+ (syntax-parse ty
+ [(~× t ...)
+ (apply stx-andmap
+ (lambda (t . ps) (check-exhaust ps t))
+ #'(t ...)
+ (syntax->list #'((p ...) ...)))])])]
+ [else ; algebraic datatypes
+ (syntax-parse (get-extra-info ty)
+ [(_ (_ (_ C) (_ Cstruct) . rst) ...)
+ (syntax-parse pats
+ [((Cpat _ ...) ...)
+ (define Cs (syntax->datum #'(C ...)))
+ (define Cstructs (syntax->datum #'(Cstruct ...)))
+ (define Cpats (syntax->datum #'(Cpat ...)))
+ (unless (set=? Cstructs Cpats)
+ (error 'match2
+ (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) clauses not exhaustive; missing: ~a"
+ (syntax-line last) (syntax-column last)
+ (string-join
+ (for/list ([C Cs][Cstr Cstructs] #:unless (member Cstr Cpats))
+ (symbol->string C))
+ ", ")))))
+ #t])]
+ [_ #t])]))
+
+ ;; TODO: do get-ctx and compile-pat in one pass
+ (define (compile-pats pats ty)
+ (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats))
+ )
+
+(define-syntax (match2 stx)
+ (syntax-parse stx #:datum-literals (with)
+ [(_ e with . clauses)
+ #:fail-when (null? (syntax->list #'clauses)) "no clauses"
+ #:with [e- τ_e] (infer+erase #'e)
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([(~seq p ...) -> e_body] ...)
+ #:with (pat ...) (stx-map ; use brace to indicate root pattern
+ (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+ #'((p ...) ...))
+ #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
+ #:with ty-expected (get-expected-type stx)
+ #:with ([(x- ...) e_body- ty_body] ...)
+ (stx-map
+ infer/ctx+erase
+ #'(ctx ...) #'((add-expected e_body ty-expected) ...))
+ #:when (check-exhaust #'(pat- ...) #'τ_e)
+ #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
+ (⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) : τ_out)
+ ])]))
+
+(define-typed-syntax match #:datum-literals (with)
+ [(_ e with . clauses)
+ #:fail-when (null? (syntax->list #'clauses)) "no clauses"
+ #:with [e- τ_e] (infer+erase #'e)
+ #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
+ (cond
+ [(×? #'τ_e) ;; e is tuple
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([x ... -> e_body])
+ #:with (~× ty ...) #'τ_e
+ #:fail-unless (stx-length=? #'(ty ...) #'(x ...))
+ "match clause pattern not compatible with given tuple"
+ #:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...)
+ #'(add-expected e_body t_expect))
+ #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
+ #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))
+ #:with z (generate-temporary)
+ (⊢ (let- ([z e-])
+ (let- ([x- (acc z)] ...) e_body-))
+ : ty_body)])]
+ [(List? #'τ_e) ;; e is List
+ (syntax-parse #'clauses #:datum-literals (-> ::)
+ [([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
+ (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'())))
+ -> e_body] ...+)
+ #:fail-unless (stx-ormap
+ (lambda (xx) (and (brack? xx) (zero? (stx-length xx))))
+ #'(xs ...))
+ "match: missing empty list case"
+ #:fail-when (and (stx-andmap brack? #'(xs ...))
+ (= 1 (stx-length #'(xs ...))))
+ "match: missing non-empty list case"
+ #:with (~List ty) #'τ_e
+ #:with ([(x- ... rst-) e_body- ty_body] ...)
+ (stx-map (lambda (ctx e) (infer/ctx+erase ctx e))
+ #'(([x ty] ... [rst (List ty)]) ...) #'((add-expected e_body t_expect) ...))
+ #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
+ #:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))
+ #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...))
+ #:with (pred? ...) (stx-map
+ (lambda (l lo) #`(λ- (lst) (#,lo (length- lst) #,l)))
+ #'(len ...) #'(lenop ...))
+ #:with ((acc1 ...) ...) (stx-map
+ (lambda (xs)
+ (for/list ([(x i) (in-indexed (syntax->list xs))])
+ #`(lambda (lst) (list-ref lst #,(datum->syntax #'here i)))))
+ #'((x ...) ...))
+ #:with (acc2 ...) (stx-map (lambda (l) #`(lambda (lst) (list-tail lst #,l))) #'(len ...))
+ (⊢ (let- ([z e-])
+ (cond-
+ [(pred? z)
+ (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))
+ : τ_out)])]
+ [else ;; e is variant
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([Clause:id x:id ...
+ (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
+ -> e_c_un] ...+) ; un = unannotated with expected ty
+ ;; length #'clauses may be > length #'info, due to guards
+ #:with info-body (get-extra-info #'τ_e)
+ #:with (_ (_ (_ ConsAll) . _) ...) #'info-body
+ #:fail-unless (set=? (syntax->datum #'(Clause ...))
+ (syntax->datum #'(ConsAll ...)))
+ (type-error #:src stx
+ #:msg (string-append
+ "match: clauses not exhaustive; missing: "
+ (string-join
+ (map symbol->string
+ (set-subtract
+ (syntax->datum #'(ConsAll ...))
+ (syntax->datum #'(Clause ...))))
+ ", ")))
+ #:with ((_ _ _ Cons? [_ acc τ] ...) ...)
+ (map ; ok to compare symbols since clause names can't be rebound
+ (lambda (Cl)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst) (equal? Cl (syntax->datum #'C))])
+ (stx-cdr #'info-body))) ; drop leading #%app
+ (syntax->datum #'(Clause ...)))
+ ;; this commented block experiments with expanding to unsafe ops
+ ;; #:with ((acc ...) ...) (stx-map
+ ;; (lambda (accs)
+ ;; (for/list ([(a i) (in-indexed (syntax->list accs))])
+ ;; #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
+ ;; #'((acc-fn ...) ...))
+ #:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
+ #:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
+ (stx-map
+ (λ (bs eg+ec) (infers/ctx+erase bs eg+ec))
+ #'(([x : τ] ...) ...) #'((e_guard e_c) ...))
+ #:fail-unless (and (same-types? #'(τ_guard ...))
+ (Bool? (stx-car #'(τ_guard ...))))
+ "guard expression(s) must have type bool"
+ #:with τ_out (stx-foldr (current-join) (stx-car #'(τ_ec ...)) (stx-cdr #'(τ_ec ...)))
+ #:with z (generate-temporary) ; dont duplicate eval of test expr
+ (⊢ (let- ([z e-])
+ (cond-
+ [(and- (Cons? z)
+ (let- ([x- (acc z)] ...) e_guard-))
+ (let- ([x- (acc z)] ...) e_c-)] ...))
+ : τ_out)])])])
+
+(define-syntax → ; wrapping →
+ (syntax-parser
+ [(_ ty ... #:TC TC ...)
+ #'(∀ () (=> TC ... (ext-stlc:→ ty ...)))]
+ [(_ Xs . rst)
+ #:when (brace? #'Xs)
+ #:with (X ...) #'Xs
+ (syntax-property
+ #'(∀ (X ...) (ext-stlc:→ . rst))
+ 'orig (list #'(→ . rst)))]
+ [(_ . rst) (set-stx-prop/preserved #'(∀ () (ext-stlc:→ . rst)) 'orig (list #'(→ . rst)))]))
+; special arrow that computes free vars; for use with tests
+; (because we can't write explicit forall
+(define-syntax →/test
+ (syntax-parser
+ [(_ (~and Xs (X:id ...)) . rst)
+ #:when (brace? #'Xs)
+ #'(∀ (X ...) (ext-stlc:→ . rst))]
+ [(_ . rst)
+ #:with Xs (compute-tyvars #'rst)
+ #'(∀ Xs (ext-stlc:→ . rst))]))
+
+(define-syntax =>/test
+ (syntax-parser
+ [(_ . (~and rst (TC ... (_arr . tys_arr))))
+ #:with Xs (compute-tyvars #'rst)
+ #'(∀ Xs (=> TC ... (ext-stlc:→ . tys_arr)))]))
+
+; redefine these to use lifted →
+(define-primop + : (→ Int Int Int))
+(define-primop - : (→ Int Int Int))
+(define-primop * : (→ Int Int Int))
+(define-primop max : (→ Int Int Int))
+(define-primop min : (→ Int Int Int))
+(define-primop void : (→ Unit))
+(define-primop = : (→ Int Int Bool))
+(define-primop <= : (→ Int Int Bool))
+(define-primop >= : (→ Int Int Bool))
+(define-primop < : (→ Int Int Bool))
+(define-primop > : (→ Int Int Bool))
+(define-primop modulo : (→ Int Int Int))
+(define-primop zero? : (→ Int Bool))
+(define-primop sub1 : (→ Int Int))
+(define-primop add1 : (→ Int Int))
+(define-primop not : (→ Bool Bool))
+(define-primop abs : (→ Int Int))
+(define-primop even? : (→ Int Bool))
+(define-primop odd? : (→ Int Bool))
+
+;; λ --------------------------------------------------------------------------
+
+; all λs have type (∀ (X ...) (→ τ_in ... τ_out)), even monomorphic fns
+(define-typed-syntax liftedλ #:export-as λ
+ [(_ ([x:id (~datum :) ty] ... #:where TC ...) body)
+ #:with (X ...) (compute-tyvars #'(ty ...))
+ (syntax/loc stx (liftedλ {X ...} ([x : ty] ... #:where TC ...) body))]
+ ;; TODO: I dont think this works for nested lambdas
+ ;; ie, this will will re-infer tyvars X that should be bound by outer lam
+ ;; - tyvars need to be bound in 2nd expand/df
+ ;; - This is fixed in master by Alex
+ [(_ (~and Xs (X ...)) ([x:id (~datum :) ty] ... #:where TC ...) body)
+ #:when (brace? #'Xs)
+ #:with (_ Xs+
+ (_ () (_ () (_ () (_ () ; 2 let-stx = 4 let-values
+ (_ (_ _ TC+ ...)
+ (_ _ ty+ ...)
+ (_ op-tmps+
+ (_ () (_ ()
+ ((~literal #%expression)
+ (_ xs+
+ (_ () (_ () body+)))))))))))))
+ (expand/df
+ #'(lambda (X ...)
+ (let-syntax
+ ([X (make-rename-transformer (assign-type #'X #'#%type))] ...)
+ (let-syntax
+ ;; must have this inner macro bc body of lambda may require
+ ;; ops defined by TC to be bound
+ ([a (syntax-parser [(_)
+ (syntax-parse (expand/df #'(void TC ...)) ; must expand in ctx of Xs
+ [(_ _ .
+ (~and (TC+ (... ...))
+ (~TCs ([op-sym ty-op] (... ...)) (... ...))))
+ ;; here, * suffix = flattened list
+ ;; op* ... = op-sym ... with proper ctx, and then flattened
+ #:with (op* (... ...))
+ (stx-appendmap
+ (lambda (os tc)
+ (stx-map (lambda (o) (format-id tc "~a" o)) os))
+ #'((op-sym (... ...)) (... ...)) #'(TC ...))
+ #:with (op-tmp* (... ...)) (generate-temporaries #'(op* (... ...)))
+ #:with (ty-op* (... ...)) (stx-flatten #'((ty-op (... ...)) (... ...)))
+ #:with ty-in-tagsss
+ (stx-map
+ (syntax-parser
+ [(~∀ _ fa-body)
+ (get-type-tags
+ (syntax-parse #'fa-body
+ [(~ext-stlc:→ in (... ...) _) #'(in (... ...))]
+ [(~=> _ (... ...) (~ext-stlc:→ in (... ...) _)) #'(in (... ...))]))])
+ #'(ty-op* (... ...)))
+ #:with (mangled-op (... ...)) (stx-map mangle #'(op* (... ...)) #'ty-in-tagsss)
+ #:with (y (... ...)) #'(x ...)
+ #:with (_ _ ty+ (... ...)) (expand/df #'(void ty ...))
+ #:with res
+ (expand/df
+ #'(lambda (op-tmp* (... ...))
+ (let-syntax
+ ([mangled-op
+ (make-rename-transformer (assign-type #'op-tmp* #'ty-op*))] (... ...))
+ (lambda (y (... ...))
+ (let-syntax
+ ([y (make-rename-transformer (assign-type #'y #'ty+))] (... ...))
+ body)))))
+ #'((void TC+ (... ...)) (void ty+ (... ...)) res)])])])
+ (a)))))
+ #:with ty-out (typeof #'body+)
+ #:with ty-out-expected (get-expected-type #'body+)
+ #:fail-unless (or (not (syntax-e #'ty-out-expected))
+ (typecheck? #'ty-out #'ty-out-expected))
+ (type-error #:src #'body
+ #:msg "Body has type ~a, expected/given: ~a"
+ #'ty-out #'ty-out-expected)
+ (⊢ (λ op-tmps+ (λ xs+ body+))
+ : (∀ Xs+ (=> TC+ ... (ext-stlc:→ ty+ ... ty-out))))]
+ [(_ ([x:id (~datum :) ty] ...) body) ; no TC
+ #:with (X ...) (compute-tyvars #'(ty ...))
+ #:with (~∀ () (~ext-stlc:→ _ ... body-ty)) (get-expected-type stx)
+ #'(Λ (X ...) (ext-stlc:λ ([x : ty] ...) (add-expected body body-ty)))]
+ [(_ ([x:id (~datum :) ty] ...) body) ; no TC, ignoring expected-type
+ #:with (X ...) (compute-tyvars #'(ty ...))
+ #'(Λ (X ...) (ext-stlc:λ ([x : ty] ...) body))]
+ [(_ (x:id ...+) body)
+ #:with (~?∀ Xs expected) (get-expected-type stx)
+ #:do [(unless (→? #'expected)
+ (type-error #:src stx #:msg "λ parameters must have type annotations"))]
+ #:with (~ext-stlc:→ arg-ty ... body-ty) #'expected
+ #:do [(unless (stx-length=? #'[x ...] #'[arg-ty ...])
+ (type-error #:src stx #:msg
+ (format "expected a function of ~a arguments, got one with ~a arguments"
+ (stx-length #'[arg-ty ...] #'[x ...]))))]
+ #`(Λ Xs (ext-stlc:λ ([x : arg-ty] ...) #,(add-expected-ty #'body #'body-ty)))]
+ #;[(_ args body)
+ #:with (~∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx)
+ #`(Λ () (ext-stlc:λ args #,(add-expected-ty #'body #'body-ty)))]
+ #;[(_ (~and x+tys ([_ (~datum :) ty] ...)) . body)
+ #:with Xs (compute-tyvars #'(ty ...))
+ ;; TODO is there a way to have λs that refer to ids defined after them?
+ #'(Λ Xs (ext-stlc:λ x+tys . body))])
+
+
+;; #%app --------------------------------------------------
+(define-typed-syntax mlish:#%app #:export-as #%app
+ [(_ e_fn . e_args)
+; #:when (printf "app: ~a\n" (syntax->datum #'(e_fn . e_args)))
+ ;; ) compute fn type (ie ∀ and →)
+ #:with [e_fn- (~and ty_fn (~∀ Xs ty_fnX))] (infer+erase #'e_fn)
+ (cond
+ [(stx-null? #'Xs)
+ (define/with-syntax tyX_args
+ (syntax-parse #'ty_fnX
+ [(~ext-stlc:→ . tyX_args) #'tyX_args]))
+ (syntax-parse #'(e_args tyX_args)
+ [((e_arg ...) (τ_inX ... _))
+ #:fail-unless (stx-length=? #'(e_arg ...) #'(τ_inX ...))
+ (mk-app-err-msg stx #:expected #'(τ_inX ...)
+ #:note "Wrong number of arguments.")
+ #:with e_fn/ty (⊢ e_fn- : (ext-stlc:→ . tyX_args))
+ #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
+ [else
+ (syntax-parse #'ty_fnX
+ ;; TODO: combine these two clauses
+ ;; no typeclasses, duplicate code for now --------------------------------
+ [(~ext-stlc:→ . tyX_args)
+ ;; ) solve for type variables Xs
+ (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args stx))
+ ;; ) instantiate polymorphic function type
+ (syntax-parse (inst-types/cs #'Xs #'cs #'tyX_args)
+ [(τ_in ... τ_out) ; concrete types
+ ;; ) arity check
+ #:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
+ (mk-app-err-msg stx #:expected #'(τ_in ...)
+ #:note "Wrong number of arguments.")
+ ;; ) compute argument types; re-use args expanded during solve
+ #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))])
+ (infers+erase
+ (stx-map add-expected-ty
+ (stx-drop #'e_args n) (stx-drop #'(τ_in ...) n))))
+ #:with (τ_arg1 ...) (stx-map typeof #'(e_arg1- ...))
+ #:with (τ_arg ...) #'(τ_arg1 ... τ_arg2 ...)
+ #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...)
+ ;; ) typecheck args
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+ (mk-app-err-msg stx
+ #:given #'(τ_arg ...)
+ #:expected
+ (stx-map
+ (lambda (tyin)
+ (define old-orig (get-orig tyin))
+ (define new-orig
+ (and old-orig
+ (substs
+ (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig
+ (lambda (x y)
+ (equal? (syntax->datum x) (syntax->datum y))))))
+ (syntax-property tyin 'orig (list new-orig)))
+ #'(τ_in ...)))
+ #:with τ_out* (if (stx-null? #'(unsolved-X ...))
+ #'τ_out
+ (syntax-parse #'τ_out
+ [(~?∀ (Y ...) τ_out)
+ (unless (→? #'τ_out)
+ (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
+ #'(∀ (unsolved-X ... Y ...) τ_out)]))
+ (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])]
+ ;; handle type class constraints ----------------------------------------
+ [(~=> TCX ... (~ext-stlc:→ . tyX_args))
+ ;; ) solve for type variables Xs
+ (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args stx))
+ ;; ) instantiate polymorphic function type
+ (syntax-parse (inst-types/cs #'Xs #'cs #'((TCX ...) tyX_args))
+ [((TC ...) (τ_in ... τ_out)) ; concrete types
+ #:with (~TCs ([generic-op ty-concrete-op] ...) ...) #'(TC ...)
+ #:with (op ...)
+ (stx-appendmap
+ (lambda (gen-ops conc-op-tys TC)
+ (map
+ (lambda (o tys)
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (lambda (e)
+ (type-error #:src stx
+ #:msg
+ (format
+ (string-append
+ "~a instance undefined. "
+ "Cannot instantiate function with constraints "
+ "~a with:\n ~a")
+ (type->str
+ (let*
+ ([old-orig (get-orig TC)]
+ [new-orig
+ (and
+ old-orig
+ (substs (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig
+ (lambda (x y)
+ (equal? (syntax->datum x)
+ (syntax->datum y)))))])
+ (syntax-property TC 'orig (list new-orig))))
+ (types->str #'(TCX ...))
+ (string-join
+ (stx-map
+ (lambda (X ty-solved)
+ (string-append (type->str X) " : " (type->str ty-solved)))
+ #'Xs (lookup-Xs/keep-unsolved #'Xs #'cs)) ", "))))])
+ (lookup-op o tys)))
+ (stx-map (lambda (o) (format-id stx "~a" o #:source stx)) gen-ops)
+ (stx-map
+ (syntax-parser
+ [(~∀ _ (~ext-stlc:→ ty_in ... _)) #'(ty_in ...)])
+ conc-op-tys)))
+ #'((generic-op ...) ...) #'((ty-concrete-op ...) ...) #'(TC ...))
+ ;; ) arity check
+ #:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
+ (mk-app-err-msg stx #:expected #'(τ_in ...)
+ #:note "Wrong number of arguments.")
+ ;; ) compute argument types; re-use args expanded during solve
+ #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))])
+ (infers+erase
+ (stx-map add-expected-ty
+ (stx-drop #'e_args n) (stx-drop #'(τ_in ...) n))))
+ #:with (τ_arg1 ...) (stx-map typeof #'(e_arg1- ...))
+ #:with (τ_arg ...) #'(τ_arg1 ... τ_arg2 ...)
+ #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...)
+ ;; ) typecheck args
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+ (mk-app-err-msg stx
+ #:given #'(τ_arg ...)
+ #:expected
+ (stx-map
+ (lambda (tyin)
+ (define old-orig (get-orig tyin))
+ (define new-orig
+ (and old-orig
+ (substs
+ (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig
+ (lambda (x y)
+ (equal? (syntax->datum x) (syntax->datum y))))))
+ (syntax-property tyin 'orig (list new-orig)))
+ #'(τ_in ...)))
+ #:with τ_out* (if (stx-null? #'(unsolved-X ...))
+ #'τ_out
+ (syntax-parse #'τ_out
+ [(~?∀ (Y ...) τ_out)
+ (unless (→? #'τ_out)
+ (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
+ #'(∀ (unsolved-X ... Y ...) τ_out)]))
+ (⊢ ((#%app- e_fn- op ...) e_arg- ...) : τ_out*)])])])]
+ [(_ e_fn . e_args) ; err case; e_fn is not a function
+ #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+ (type-error #:src stx
+ #:msg (format "Expected expression ~a to have → type, got: ~a"
+ (syntax->datum #'e_fn) (type->str #'τ_fn)))])
+
+
+;; cond and other conditionals
+(define-typed-syntax cond
+ [(_ [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
+ test)
+ b ... body] ...+)
+ #:with (test- ...) (⇑s (test ...) as Bool)
+ #:with ty-expected (get-expected-type stx)
+ #:with ([body- ty_body] ...) (infers+erase #'((add-expected body ty-expected) ...))
+ #:with (([b- ty_b] ...) ...) (stx-map infers+erase #'((b ...) ...))
+ #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
+ (⊢ (cond- [test- b- ... body-] ...) : τ_out)])
+(define-typed-syntax when
+ [(_ test body ...)
+; #:with test- (⇑ test as Bool)
+ #:with [test- _] (infer+erase #'test)
+ #:with [(body- _) ...] (infers+erase #'(body ...))
+ (⊢ (when- test- body- ...) : Unit)])
+(define-typed-syntax unless
+ [(_ test body ...)
+; #:with test- (⇑ test as Bool)
+ #:with [test- _] (infer+erase #'test)
+ #:with [(body- _) ...] (infers+erase #'(body ...))
+ (⊢ (unless- test- body- ...) : Unit)])
+
+;; sync channels and threads
+(define-type-constructor Channel)
+
+(define-typed-syntax make-channel
+ [(_ (~and tys {ty}))
+ #:when (brace? #'tys)
+ (⊢ (make-channel-) : (Channel ty))])
+(define-typed-syntax channel-get
+ [(_ c)
+ #:with (c- (ty)) (⇑ c as Channel)
+ (⊢ (channel-get- c-) : ty)])
+(define-typed-syntax channel-put
+ [(_ c v)
+ #:with (c- (ty)) (⇑ c as Channel)
+ #:with [v- ty_v] (infer+erase #'v)
+ #:fail-unless (typechecks? #'ty_v #'ty)
+ (format "Cannot send ~a value on ~a channel."
+ (type->str #'ty_v) (type->str #'ty))
+ (⊢ (channel-put- c- v-) : Unit)])
+
+(define-base-type Thread)
+
+;; threads
+(define-typed-syntax thread
+ [(_ th)
+ #:with (th- (~∀ () (~ext-stlc:→ τ_out))) (infer+erase #'th)
+ (⊢ (thread- th-) : Thread)])
+
+(define-primop random : (→ Int Int))
+(define-primop integer->char : (→ Int Char))
+(define-primop string->list : (→ String (List Char)))
+(define-primop string->number : (→ String Int))
+;(define-primop number->string : (→ Int String))
+(define-typed-syntax num->str #:export-as number->string
+ [f:id (assign-type #'number->string #'(→ Int String))]
+ [(_ n)
+ #'(num->str n (ext-stlc:#%datum . 10))]
+ [(_ n rad)
+ #:with args- (⇑s (n rad) as Int)
+ (⊢ (number->string- . args-) : String)])
+(define-primop string : (→ Char String))
+(define-primop sleep : (→ Int Unit))
+(define-primop string=? : (→ String String Bool))
+(define-primop string<? : (→ String String Bool))
+(define-primop string<=? : (→ String String Bool))
+(define-primop string>? : (→ String String Bool))
+(define-primop string>=? : (→ String String Bool))
+(define-primop char=? : (→ Char Char Bool))
+(define-primop char<? : (→ Char Char Bool))
+(define-primop char<=? : (→ Char Char Bool))
+(define-primop char>? : (→ Char Char Bool))
+(define-primop char>=? : (→ Char Char Bool))
+
+(define-typed-syntax string-append
+ [(_ . strs)
+ #:with strs- (⇑s strs as String)
+ (⊢ (string-append- . strs-) : String)])
+
+;; vectors
+(define-type-constructor Vector)
+
+(define-typed-syntax vector
+ [(_ (~and tys {ty}))
+ #:when (brace? #'tys)
+ (⊢ (vector-) : (Vector ty))]
+ [(_ v ...)
+ #:with ([v- ty] ...) (infers+erase #'(v ...))
+ #:when (same-types? #'(ty ...))
+ #:with one-ty (stx-car #'(ty ...))
+ (⊢ (vector- v- ...) : (Vector one-ty))])
+(define-typed-syntax make-vector/tc #:export-as make-vector
+ [(_ n) #'(make-vector/tc n (ext-stlc:#%datum . 0))]
+ [(_ n e)
+ #:with n- (⇑ n as Int)
+ #:with [e- ty] (infer+erase #'e)
+ (⊢ (make-vector- n- e-) : (Vector ty))])
+(define-typed-syntax vector-length
+ [(_ e)
+ #:with [e- _] (⇑ e as Vector)
+ (⊢ (vector-length- e-) : Int)])
+(define-typed-syntax vector-ref
+ [(_ e n)
+ #:with n- (⇑ n as Int)
+ #:with [e- (ty)] (⇑ e as Vector)
+ (⊢ (vector-ref- e- n-) : ty)])
+(define-typed-syntax vector-set!
+ [(_ e n v)
+ #:with n- (⇑ n as Int)
+ #:with [e- (ty)] (⇑ e as Vector)
+ #:with [v- ty_v] (infer+erase #'v)
+ #:when (typecheck? #'ty_v #'ty)
+ (⊢ (vector-set!- e- n- v-) : Unit)])
+(define-typed-syntax vector-copy!
+ [(_ dest start src)
+ #:with start- (⇑ start as Int)
+ #:with [dest- (ty_dest)] (⇑ dest as Vector)
+ #:with [src- (ty_src)] (⇑ src as Vector)
+ #:when (typecheck? #'ty_dest #'ty_src)
+ (⊢ (vector-copy!- dest- start- src-) : Unit)])
+
+
+;; sequences and for loops
+
+(define-type-constructor Sequence)
+
+(define-typed-syntax in-range/tc #:export-as in-range
+ [(_ end)
+ #'(in-range/tc (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]
+ [(_ start end)
+ #'(in-range/tc start end (ext-stlc:#%datum . 1))]
+ [(_ start end step)
+ #:with (e- ...) (⇑s (start end step) as Int)
+ (⊢ (in-range- e- ...) : (Sequence Int))])
+
+(define-typed-syntax in-naturals/tc #:export-as in-naturals
+ [(_) #'(in-naturals/tc (ext-stlc:#%datum . 0))]
+ [(_ start)
+ #:with start- (⇑ start as Int)
+ (⊢ (in-naturals- start-) : (Sequence Int))])
+
+
+(define-typed-syntax in-vector
+ [(_ e)
+ #:with [e- (ty)] (⇑ e as Vector)
+ (⊢ (in-vector- e-) : (Sequence ty))])
+
+(define-typed-syntax in-list
+ [(_ e)
+ #:with [e- (ty)] (⇑ e as List)
+ (⊢ (in-list- e-) : (Sequence ty))])
+
+(define-typed-syntax in-lines
+ [(_ e)
+ #:with e- (⇑ e as String)
+ (⊢ (in-lines- (open-input-string- e-)) : (Sequence String))])
+
+(define-typed-syntax for
+ [(_ ([x:id e]...) b ... body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) (b- ... body-) (ty_b ... ty_body)]
+ (infers/ctx+erase #'([x : ty] ...) #'(b ... body))
+ (⊢ (for- ([x- e-] ...) b- ... body-) : Unit)])
+(define-typed-syntax for*
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for*- ([x- e-] ...) body-) : Unit)])
+
+(define-typed-syntax for/list
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for/list- ([x- e-] ...) body-) : (List ty_body))])
+(define-typed-syntax for/vector
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for/vector- ([x- e-] ...) body-) : (Vector ty_body))])
+(define-typed-syntax for*/vector
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for*/vector- ([x- e-] ...) body-) : (Vector ty_body))])
+(define-typed-syntax for*/list
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for*/list- ([x- e-] ...) body-) : (List ty_body))])
+(define-typed-syntax for/fold
+ [(_ ([acc init]) ([x:id e] ...) body)
+ #:with [init- ty_init] (infer+erase #`(pass-expected init #,stx))
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(acc- x- ...) body- ty_body]
+ (infer/ctx+erase #'([acc : ty_init][x : ty] ...) #'body)
+ #:fail-unless (typecheck? #'ty_body #'ty_init)
+ (type-error #:src stx
+ #:msg
+ "for/fold: Type of body and initial accumulator must be the same, given ~a and ~a"
+ #'ty_init #'ty_body)
+ (⊢ (for/fold- ([acc- init-]) ([x- e-] ...) body-) : ty_body)])
+
+(define-typed-syntax for/hash
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- (~× ty_k ty_v)]
+ (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for/hash- ([x- e-] ...) (let- ([t body-]) (values- (car- t) (cadr- t))))
+ : (Hash ty_k ty_v))])
+
+(define-typed-syntax for/sum
+ [(_ ([x:id e]...
+ (~optional (~seq #:when guard) #:defaults ([guard #'#t])))
+ body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) (guard- body-) (_ ty_body)]
+ (infers/ctx+erase #'([x : ty] ...) #'(guard body))
+ #:when (Int? #'ty_body)
+ (⊢ (for/sum- ([x- e-] ... #:when guard-) body-) : Int)])
+
+; printing and displaying
+(define-typed-syntax printf
+ [(_ str e ...)
+ #:with s- (⇑ str as String)
+ #:with ([e- ty] ...) (infers+erase #'(e ...))
+ (⊢ (printf- s- e- ...) : Unit)])
+(define-typed-syntax format
+ [(_ str e ...)
+ #:with s- (⇑ str as String)
+ #:with ([e- ty] ...) (infers+erase #'(e ...))
+ (⊢ (format- s- e- ...) : String)])
+(define-typed-syntax display
+ [(_ e)
+ #:with [e- _] (infer+erase #'e)
+ (⊢ (display- e-) : Unit)])
+(define-typed-syntax displayln
+ [(_ e)
+ #:with [e- _] (infer+erase #'e)
+ (⊢ (displayln- e-) : Unit)])
+(define-primop newline : (→ Unit))
+
+(define-typed-syntax list->vector
+ [(_ e)
+ #:with [e- (ty)] (⇑ e as List)
+ (⊢ (list->vector- e-) : (Vector ty))])
+
+(define-typed-syntax let
+ [(_ name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body)
+ #:with ([e- ty_e] ...) (infers+erase #'(e ...))
+ #:with [(name- . xs-) (body- ...) (_ ... ty_body)]
+ (infers/ctx+erase #'([name : (→ ty_e ... ty.norm)][x : ty_e] ...)
+ #'(b ... body))
+ #:fail-unless (typecheck? #'ty_body #'ty.norm)
+ (format "type of let body ~a does not match expected typed ~a"
+ (type->str #'ty_body) (type->str #'ty))
+ (⊢ (letrec- ([name- (λ- xs- body- ...)])
+ (name- e- ...))
+ : ty_body)]
+ [(_ ([x:id e] ...) body ...)
+ #'(ext-stlc:let ([x e] ...) (begin/tc body ...))])
+(define-typed-syntax let*
+ [(_ ([x:id e] ...) body ...)
+ #'(ext-stlc:let* ([x e] ...) (begin/tc body ...))])
+
+(define-typed-syntax begin/tc #:export-as begin
+ [(_ body ... b)
+ #:with expected (get-expected-type stx)
+ #:with b_ann #'(add-expected b expected)
+ #'(ext-stlc:begin body ... b_ann)])
+
+;; hash
+(define-type-constructor Hash #:arity = 2)
+
+(define-typed-syntax in-hash
+ [(_ e)
+ #:with [e- (ty_k ty_v)] (⇑ e as Hash)
+ (⊢ (map- (λ- (k+v) (list- (car- k+v) (cdr- k+v))) (hash->list- e-))
+; (⊢ (hash->list e-)
+ : (Sequence (stlc+rec-iso:× ty_k ty_v)))])
+
+; mutable hashes
+(define-typed-syntax hash
+ [(_ (~and tys {ty_key ty_val}))
+ #:when (brace? #'tys)
+ (⊢ (make-hash-) : (Hash ty_key ty_val))]
+ [(_ (~seq k v) ...)
+ #:with ([k- ty_k] ...) (infers+erase #'(k ...))
+ #:with ([v- ty_v] ...) (infers+erase #'(v ...))
+ #:when (same-types? #'(ty_k ...))
+ #:when (same-types? #'(ty_v ...))
+ #:with ty_key (stx-car #'(ty_k ...))
+ #:with ty_val (stx-car #'(ty_v ...))
+ (⊢ (make-hash- (list- (cons- k- v-) ...)) : (Hash ty_key ty_val))])
+(define-typed-syntax hash-set!
+ [(_ h k v)
+ #:with [h- (ty_key ty_val)] (⇑ h as Hash)
+ #:with [k- ty_k] (infer+erase #'k)
+ #:with [v- ty_v] (infer+erase #'v)
+ #:when (typecheck? #'ty_k #'ty_key)
+ #:when (typecheck? #'ty_v #'ty_val)
+ (⊢ (hash-set!- h- k- v-) : Unit)])
+(define-typed-syntax hash-ref/tc #:export-as hash-ref
+ [(_ h k) #'(hash-ref/tc h k (ext-stlc:#%datum . #f))]
+ [(_ h k fail)
+ #:with [h- (ty_key ty_val)] (⇑ h as Hash)
+ #:with [k- ty_k] (infer+erase #'k)
+ #:when (typecheck? #'ty_k #'ty_key)
+ #:with (fail- _) (infer+erase #'fail) ; default val can be any
+ (⊢ (hash-ref- h- k- fail-) : ty_val)])
+(define-typed-syntax hash-has-key?
+ [(_ h k)
+ #:with [h- (ty_key _)] (⇑ h as Hash)
+ #:with [k- ty_k] (infer+erase #'k)
+ #:when (typecheck? #'ty_k #'ty_key)
+ (⊢ (hash-has-key?- h- k-) : Bool)])
+
+(define-typed-syntax hash-count
+ [(_ h)
+ #:with [h- _] (⇑ h as Hash)
+ (⊢ (hash-count- h-) : Int)])
+
+(define-base-type String-Port)
+(define-base-type Input-Port)
+(define-primop open-output-string : (→ String-Port))
+(define-primop get-output-string : (→ String-Port String))
+(define-primop string-upcase : (→ String String))
+
+(define-typed-syntax write-string/tc #:export-as write-string
+ [(_ str out)
+ #'(write-string/tc str out (ext-stlc:#%datum . 0) (string-length/tc str))]
+ [(_ str out start end)
+ #:with str- (⇑ str as String)
+ #:with out- (⇑ out as String-Port)
+ #:with start- (⇑ start as Int)
+ #:with end- (⇑ end as Int)
+ (⊢ (write-string- str- out- start- end-) : Unit)])
+
+(define-typed-syntax string-length/tc #:export-as string-length
+ [(_ str)
+ #:with str- (⇑ str as String)
+ (⊢ (string-length- str-) : Int)])
+(define-primop make-string : (→ Int String))
+(define-primop string-set! : (→ String Int Char Unit))
+(define-primop string-ref : (→ String Int Char))
+(define-typed-syntax string-copy!/tc #:export-as string-copy!
+ [(_ dest dest-start src)
+ #'(string-copy!/tc
+ dest dest-start src (ext-stlc:#%datum . 0) (string-length/tc src))]
+ [(_ dest dest-start src src-start src-end)
+ #:with dest- (⇑ dest as String)
+ #:with src- (⇑ src as String)
+ #:with dest-start- (⇑ dest-start as Int)
+ #:with src-start- (⇑ src-start as Int)
+ #:with src-end- (⇑ src-end as Int)
+ (⊢ (string-copy!- dest- dest-start- src- src-start- src-end-) : Unit)])
+
+(define-primop fl+ : (→ Float Float Float))
+(define-primop fl- : (→ Float Float Float))
+(define-primop fl* : (→ Float Float Float))
+(define-primop fl/ : (→ Float Float Float))
+(define-primop fl= : (→ Float Float Bool))
+(define-primop flsqrt : (→ Float Float))
+(define-primop flceiling : (→ Float Float))
+(define-primop inexact->exact : (→ Float Int))
+(define-primop exact->inexact : (→ Int Float))
+(define-primop char->integer : (→ Char Int))
+(define-primop real->decimal-string : (→ Float Int String))
+(define-primop fx->fl : (→ Int Float))
+(define-typed-syntax quotient+remainder
+ [(_ x y)
+ #:with x- (⇑ x as Int)
+ #:with y- (⇑ y as Int)
+ (⊢ (call-with-values- (λ- () (quotient/remainder- x- y-)) list-)
+ : (stlc+rec-iso:× Int Int))])
+(define-primop quotient : (→ Int Int Int))
+
+(define-typed-syntax set!
+ [(_ x:id e)
+ #:with [x- ty_x] (infer+erase #'x)
+ #:with [e- ty_e] (infer+erase #'e)
+ #:when (typecheck? #'ty_e #'ty_x)
+ (⊢ (set!- x e-) : Unit)])
+
+(define-typed-syntax provide-type [(_ ty ...) #'(provide- ty ...)])
+
+(define-typed-syntax provide
+ [(_ x:id ...)
+ #:with ([x- ty_x] ...) (infers+erase #'(x ...))
+ ; TODO: use hash-code to generate this tmp
+ #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
+ #'(begin-
+ (provide- x ...)
+ (stlc+rec-iso:define-type-alias x-ty ty_x) ...
+ (provide- x-ty ...))])
+(define-typed-syntax require-typed
+ [(_ x:id ... #:from mod)
+ #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
+ #:with (y ...) (generate-temporaries #'(x ...))
+ #'(begin-
+ (require- (rename-in- (only-in- mod x ... x-ty ...) [x y] ...))
+ (define-syntax- x (make-rename-transformer (assign-type #'y #'x-ty))) ...)])
+
+(define-base-type Regexp)
+(define-primop regexp-match : (→ Regexp String (List String)))
+(define-primop regexp : (→ String Regexp))
+
+(define-typed-syntax equal?
+ [(_ e1 e2)
+ #:with [e1- ty1] (infer+erase #'e1)
+ #:with [e2- ty2] (infer+erase #'(add-expected e2 ty1))
+ #:fail-unless (typecheck? #'ty1 #'ty2) "arguments to equal? have different types"
+ (⊢ (equal?- e1- e2-) : Bool)])
+
+(define-syntax (inst stx)
+ (syntax-parse stx
+ [(_ e ty ...)
+ #:with [ee tyty] (infer+erase #'e)
+ #:with [e- ty_e] (infer+erase #'(sysf:inst e ty ...))
+ #:with ty_out (cond
+ [(→? #'ty_e) #'(∀ () ty_e)]
+ [(=>? #'ty_e) #'(∀ () ty_e)]
+ [else #'ty_e])
+ (⊢ e- : ty_out)]))
+
+(define-typed-syntax read
+ [(_)
+ (⊢ (let- ([x (read-)])
+ (cond- [(eof-object?- x) ""]
+ [(number?- x) (number->string- x)]
+ [(symbol?- x) (symbol->string- x)])) : String)])
+
+(begin-for-syntax
+ ;; - this function should be wrapped with err handlers,
+ ;; for when an op with the specified generic op and input types does not exist,
+ ;; otherwise, will get "unbound id" err with internal mangled id
+ ;; - gen-op must be identifier, eg should already have proper context
+ ;; and mangled-op is selected based on input types,
+ ;; ie, dispatch to different concrete fns based on input tpyes
+ ;; TODO: currently using input types only, but sometimes may need output type
+ ;; eg, Read typeclass, this is currently unsupported
+ ;; - need to use expected-type?
+ (define (lookup-op gen-op tys)
+ (define (transfer-gen-op-ctx o) (format-id gen-op "~a" o))
+ (define (transfer-gen-op-ctxs os) (stx-map transfer-gen-op-ctx os))
+ (syntax-parse tys
+ ;; TODO: for now, only handle uniform tys, ie tys must be all
+ ;; tycons or all base types or all tyvars
+ ;; tycon --------------------------------------------------
+ ;; - recur on ty-args
+ [(((~literal #%plain-app) tycon
+ ((~literal #%plain-lambda) _ _ ty-arg ...)) ...)
+ ;; 1) look up concrete op corresponding to generic op and input tys
+ #:with mangled (mangle gen-op #'(tycon ...))
+ #:with [conc-op ty-conc-op] (infer+erase #'mangled)
+ ;; compute sub-ops based on TC constraints (will include gen-op --- for smaller type)
+ #:with (~∀ Xs (~=> TC ... (~ext-stlc:→ . ty-args))) #'ty-conc-op
+ #:with (~TCs ([op _] ...) ...) #'(TC ...) ; order matters, must match order of arg types
+ #:with ((sub-op ...) ...) (stx-map transfer-gen-op-ctxs #'((op ...) ...))
+ ;; drop the TCs in result type, the proper subops are already applied
+ #:with ty-conc-op-noTC #'(∀ Xs (ext-stlc:→ . ty-args))
+ ;; recursively call lookup-op for each subop and input ty-args
+ (⊢ (conc-op
+ #,@(apply stx-appendmap (lambda (ops . tys) (stx-map (lambda (o) (lookup-op o tys)) ops))
+ #'((sub-op ...) ...)
+ (syntax->list #'((ty-arg ...) ...))))
+ : ty-conc-op-noTC)]
+ ;; base type --------------------------------------------------
+ [(((~literal #%plain-app) tag) ...) (expand/df (mangle gen-op #'(tag ...)))]
+ ;; tyvars --------------------------------------------------
+ [_ (expand/df (mangle gen-op tys))]))
+ (define (get-fn-ty-in-tags ty-fn)
+ (syntax-parse ty-fn
+ [(~∀ _ (~ext-stlc:→ ty_in ... _))
+ (get-type-tags #'(ty_in ...))]))
+ (define (TC-exists? TC #:ctx [ctx TC]) ; throws exn if fail
+ (syntax-parse TC
+ [(~TC-base [gen-op ty-op] . _) ; only need 1st op
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (lambda (e)
+ (type-error #:src ctx
+ #:msg "No instance defined for ~a" TC))])
+ (expand/df
+ (mangle (format-id ctx "~a" #'gen-op)
+ (get-fn-ty-in-tags #'ty-op))))]))
+ (define (TCs-exist? TCs #:ctx [ctx TCs])
+ (stx-map (lambda (tc) (TC-exists? tc #:ctx ctx)) TCs)))
+
+;; adhoc polymorphism
+;; TODO: make this a formal type?
+;; - or at least define a pattern expander - DONE 2016-05-01
+;; A TC is a #'(=> subclassTC ... ([generic-op gen-op-ty] ...))
+(define-syntax (define-typeclass stx)
+ (syntax-parse stx
+ [(~or (_ TC ... (~datum =>) (Name X ...) [op (~datum :) ty] ...)
+ (~and (_ (Name X ...) [op (~datum :) ty] ...) ; no subclass
+ (~parse (TC ...) #'())))
+ #'(begin-
+ (define-syntax- (op stx)
+ (syntax-parse stx
+ [(o . es)
+ #:with ([e- ty_e] (... ...)) (infers+erase #'es)
+ #:with out-op
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (lambda (e)
+ (type-error #:src #'o
+ #:msg (format
+ "~a operation undefined for input types: ~a"
+ (syntax->datum #'o)
+ (types->str #'(ty_e (... ...))))))])
+ (lookup-op #'o #'(ty_e (... ...))))
+ #:with app (datum->syntax #'o '#%app)
+ (datum->syntax stx (cons #'app (cons #'out-op #'(e- (... ...)))))])) ...
+ (define-syntax- (Name stx)
+ (syntax-parse stx
+ [(_ X ...)
+ (add-orig
+ #`(=> TC ... #,(mk-type #'(('op ty) ...)))
+ #'(Name X ...))])))]))
+
+(define-syntax (define-instance stx)
+ (syntax-parse stx
+ ;; base type, possibly with subclasses ------------------------------------
+ [(_ (Name ty ...) [generic-op concrete-op] ...)
+ #:with (~=> TC ... (~TC [generic-op-expected ty-concrete-op-expected] ...))
+ (expand/df #'(Name ty ...))
+ #:when (TCs-exist? #'(TC ...) #:ctx stx)
+ #:fail-unless (set=? (syntax->datum #'(generic-op ...))
+ (syntax->datum #'(generic-op-expected ...)))
+ (type-error #:src stx
+ #:msg (format "Type class instance ~a incomplete, missing: ~a"
+ (syntax->datum #'(Name ty ...))
+ (string-join
+ (map symbol->string
+ (set-subtract (syntax->datum #'(generic-op-expected ...))
+ (syntax->datum #'(generic-op ...))))
+ ", ")))
+ ;; sort, using order from define-typeclass
+ #:with ([generic-op-sorted concrete-op-sorted] ...)
+ (stx-map
+ (lambda (expected-op)
+ (stx-findf
+ (lambda (gen+conc)
+ (equal? (syntax->datum (stx-car gen+conc))
+ (syntax->datum expected-op)))
+ #'([generic-op concrete-op] ...)))
+ #'(generic-op-expected ...))
+ ;; typecheck type of given concrete-op with expected type from define-typeclass
+ #:with ([concrete-op+ ty-concrete-op] ...) (infers+erase #'(concrete-op-sorted ...))
+ #:fail-unless (typechecks? #'(ty-concrete-op ...) #'(ty-concrete-op-expected ...))
+ (mk-app-err-msg (syntax/loc stx (#%app (Name ty ...) concrete-op ...))
+ #:expected #'(ty-concrete-op-expected ...)
+ #:given #'(ty-concrete-op ...)
+ #:action "defining typeclass instance"
+ #:name (format "~a" (syntax->datum #'(Name ty ...))))
+ ;; generate mangled name from tags in input types
+ #:with (ty_in-tags ...)
+ (stx-map
+ (syntax-parser
+ [(~∀ _ (~ext-stlc:→ ty_in ... _))
+ (get-type-tags #'(ty_in ...))])
+ #'(ty-concrete-op-expected ...))
+ ;; use input types
+ #:with (mangled-op ...) (stx-map mangle #'(generic-op ...) #'(ty_in-tags ...))
+ #'(begin-
+ (define-syntax- (mangled-op stx)
+ (syntax-parse stx [_:id (assign-type #'concrete-op+ #'ty-concrete-op-expected)]))
+ ...)]
+ ;; tycon, possibly with subclasses -----------------------------------------
+ [(_ TC ... (~datum =>) (Name ty ...) [generic-op concrete-op] ...)
+ #:with (X ...) (compute-tyvars #'(ty ...))
+ ;; ok to drop TCsub ...? I think yes
+ ;; - the same TCsubs will be part of TC+,
+ ;; so proper op will be looked up, depending on input args,
+ ;; using inherited ops in TC+
+ ;; This is assuming Name and TC ... are the same typeclass
+ ;; Won't work for, eg (TC1 (List X)) that depends on some other (TC2 X)
+ #:with (Xs+
+ (TC+ ...
+ (~=> TCsub ...
+ (~TC [generic-op-expected ty-concrete-op-expected] ...)))
+ _)
+ (infers/tyctx+erase #'([X : #%type] ...) #'(TC ... (Name ty ...)))
+ #:when (TCs-exist? #'(TCsub ...) #:ctx stx)
+ ;; simulate as if the declared concrete-op* has TC ... predicates
+ ;; TODO: fix this manual deconstruction and assembly
+ #:with ((app fa (lam _ ei ty_fn)) ...) #'(ty-concrete-op-expected ...)
+ #:with (ty-concrete-op-expected-withTC ...)
+ (stx-map (current-type-eval) #'((app fa (lam Xs+ ei (=> TC+ ... ty_fn))) ...))
+ #:fail-unless (set=? (syntax->datum #'(generic-op ...))
+ (syntax->datum #'(generic-op-expected ...)))
+ (type-error #:src stx
+ #:msg (format "Type class instance ~a incomplete, missing: ~a"
+ (syntax->datum #'(Name ty ...))
+ (string-join
+ (map symbol->string
+ (set-subtract (syntax->datum #'(generic-op-expected ...))
+ (syntax->datum #'(generic-op ...))))
+ ", ")))
+ ;; - sort, using order from define-typeclass
+ ;; - insert TC ... if lambda
+ #:with ([generic-op-sorted concrete-op-sorted] ...)
+ (stx-map
+ (lambda (expected-op)
+ (syntax-parse
+ (stx-findf
+ (lambda (gen+conc)
+ (equal? (syntax->datum (stx-car gen+conc))
+ (syntax->datum expected-op)))
+ #'([generic-op concrete-op] ...))
+ [(g c)
+ (syntax-parse #'c
+ ;; add TCs to (unexpanded) lambda
+ [((~and lam (~literal liftedλ)) (args ...) . body)
+ #'(g (lam (args ... #:where TC ...) . body))]
+ [_ #'(g c)])]))
+ #'(generic-op-expected ...))
+ ;; ;; for now, dont expand (and typecheck) concrete-op
+ ;; #:with ([concrete-op+ ty-concrete-op] ...) (infers+erase #'(concrete-op ...))
+ ;; #:when (typechecks? #'(ty-concrete-op ...) #'(ty-concrete-op-expected ...))
+ ;; TODO: right now, dont recur to get nested tags
+ ;; but may need to do so, ie if an instance needs to define more than one concrete op,
+ ;; eg (define-instance (Eq (List Int)) ...)
+ #:with (ty_in-tags ...)
+ (stx-map
+ (syntax-parser
+ [(~∀ _ (~ext-stlc:→ ty_in ... _))
+ (get-type-tags #'(ty_in ...))]
+ #;[(~∀ _ (~=> _ ... (~ext-stlc:→ ty_in ... _)))
+ (get-type-tags #'(ty_in ...))])
+ #'(ty-concrete-op-expected ...))
+ #:with (mangled-op ...) (stx-map mangle #'(generic-op ...) #'(ty_in-tags ...))
+ ;; need a name for concrete-op because concrete-op and generic-op may be
+ ;; mutually recursive, eg (Eq (List X))
+ #:with (f ...) (generate-temporaries #'(concrete-op-sorted ...))
+ #'(begin-
+ (define- f concrete-op-sorted) ...
+ (define-syntax- (mangled-op stx)
+ (syntax-parse stx [_:id (assign-type #'f #'ty-concrete-op-expected-withTC)]))
+ ...)]))
diff --git a/macrotypes/examples/tests/mlish/generic.mlish b/macrotypes/examples/tests/mlish/generic.mlish
@@ -0,0 +1,461 @@
+#lang s-exp "../../mlish+adhoc.rkt"
+(require "../rackunit-typechecking.rkt")
+
+(define-typeclass (Eq X)
+ [== : (→ X X Bool)])
+
+(define-instance (Eq Int)
+ [== =])
+
+(define-instance (Eq Float)
+ [== fl=])
+
+(define (id-fn1 [x : X] #:where (Eq X) -> X) x)
+(typecheck-fail (id-fn1 #f) #:with-msg "\\(Eq Bool\\) instance undefined")
+(check-type (id-fn1 1) : Int -> 1)
+
+(check-type (== 1 2) : Bool -> (= 1 2))
+(check-type (== 1 2) : Bool -> #f)
+(check-type (== 2 2) : Bool -> (= 2 2))
+(check-type (== 2 2) : Bool -> #t)
+(typecheck-fail (== "1" "1")
+ #:with-msg "== operation undefined for input types: String, String")
+
+(define-instance (Eq String) ; test use of lambda on rhs
+ [== (λ ([x : String] [y : String])
+ (string=? x y))])
+
+(check-type (== "1" "2") : Bool -> (string=? "1" "2"))
+(check-type (== "1" "2") : Bool -> #f)
+(check-type (== "2" "2") : Bool -> (string=? "2" "2"))
+(check-type (== "2" "2") : Bool -> #t)
+
+(define-instance (Eq Char)
+ [== char=?])
+
+(check-type (λ ([x : X] #:where (Eq X))
+ (== x x))
+ : (=>/test (Eq X) (→ X Bool)))
+
+(check-type ((λ ([x : X] #:where (Eq X)) (== x x)) 1) : Bool -> #t)
+(check-type ((λ ([x : X] #:where (Eq X)) (== x x)) "1") : Bool -> #t)
+(typecheck-fail ((λ ([x : X] #:where (Eq X)) (== x x)) #f)
+ #:with-msg
+ "Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool")
+
+(define (member? [x : X] [lst : (List X)] #:where (Eq X) -> Bool)
+ (match lst with
+ [[] -> #f]
+ [y :: ys -> (or (== x y) (member? x ys))]))
+
+(check-type (member? 1 nil) : Bool -> #f)
+(check-type (member? 1 (list 2)) : Bool -> #f)
+(check-type (member? 1 (list 2 1)) : Bool -> #t)
+(typecheck-fail (member? "1" (list 1))) ; TODO: fix err msg
+(check-type (member? "1" nil) : Bool -> #f)
+(check-type (member? "1" (list "2")) : Bool -> #f)
+(check-type (member? "1" (list "2" "1")) : Bool -> #t)
+
+;; TODO?: fix name clash of generic op and concrete op
+(define-typeclass (Ord X)
+ [lt : (→ X X Bool)]
+ [lte : (→ X X Bool)]
+ [gt : (→ X X Bool)]
+ [gte : (→ X X Bool)])
+
+(define-instance (Ord Int)
+ [lt <] [lte <=] [gt >] [gte >=])
+
+;; missing typeclass constraint
+(typecheck-fail (λ ([x : X]) (== x x))
+ #:with-msg "== operation undefined for input types: X, X")
+(typecheck-fail (λ ([x : X]) (lte x x))
+ #:with-msg "lte operation undefined for input types: X, X")
+;; wrong typeclass constraint
+(typecheck-fail (λ ([x : Y] #:where (Ord Y)) (== x x))
+ #:with-msg "== operation undefined for input types: Y, Y")
+(typecheck-fail (λ ([x : Y] #:where (Eq Y)) (gt x x))
+ #:with-msg "gt operation undefined for input types: Y, Y")
+
+(check-type (λ ([x : Y] #:where (Ord Y)) (lte x x))
+ : (=>/test (Ord Y) (→ Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y)) (lt x x))
+ : (=>/test (Ord Y) (→ Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y)) (gte x x))
+ : (=>/test (Ord Y) (→ Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y)) (gt x x))
+ : (=>/test (Ord Y) (→ Y Bool)))
+
+(check-type (λ ([x : Y] [y : Y] #:where (Ord Y)) (lt x x))
+ : (=>/test (Ord Y) (→ Y Y Bool)))
+(check-type (λ ([x : Y] [y : Y] #:where (Ord Y)) (lt x y))
+ : (=>/test (Ord Y) (→ Y Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y) (Eq Y))
+ (lt x x))
+ : (=>/test (Ord Y) (Eq Y) (→ Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y) (Eq Y))
+ (== x x))
+ : (=>/test (Ord Y) (Eq Y) (→ Y Bool)))
+
+(check-type (λ ([x : Y] #:where (Ord Y) (Eq Y))
+ (and (== x x) (lte x x)))
+ : (=>/test (Ord Y) (Eq Y) (→ Y Bool)))
+
+;; todo: not working; results in dup ids
+#;(check-type (λ ([x : X] [y : Y] #:where (Ord X) (Ord Y)) (< x y))
+ : (=>/test (Ord Y) (→ Y Y Bool)))
+
+(define (f [x : X] #:where (Eq X) -> Bool)
+ (== x x))
+(check-type (f 1) : Bool -> #t)
+(check-type (f "1") : Bool -> #t)
+(typecheck-fail (f #f)
+ #:with-msg
+ "Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool")
+
+(define-instance (Ord String)
+ [lt string<?] [lte string<=?] [gt string>?] [gte string>=?])
+(check-type (lt "1" "2") : Bool -> #t)
+(define (f2 [x : X] [y : X] #:where (Ord X) -> Bool)
+ (lte x y))
+(check-type (f2 1 2) : Bool -> #t)
+(check-type (f2 "1" "2") : Bool -> #t)
+(typecheck-fail (f2 1 "2"))
+
+(define-typeclass (Num X)
+ [add : (→ X X X)]
+ [sub : (→ X X X)]
+ [mul : (→ X X X)])
+
+(typecheck-fail
+ (define-instance (Num Int)
+ [add +] [sub -] [mul fl*])
+ #:with-msg (string-append "Type error defining typeclass instance \\(Num Int\\).*"
+ (expected "(→ Int Int Int), (→ Int Int Int), (→ Int Int Int)"
+ #:given "(→ Int Int Int), (→ Int Int Int), (→ Float Float Float)")))
+
+(define-instance (Num Int)
+ [add +] [sub -] [mul *])
+(define-instance (Num Float)
+ [add fl+] [sub fl-] [mul fl*])
+
+(define (square [x : X] #:where (Num X) -> X)
+ (mul x x))
+(check-type (square 5) : Int -> 25)
+(check-type (square 2.5) : Float -> 6.25)
+;; "propagation" of typeclass constraints to other constrained fns
+;; (memsq tests the same thing?)
+(define (square2 [x : X] #:where (Num X) -> X)
+ (square x))
+(check-type (square2 5) : Int -> 25)
+(check-type (square2 2.5) : Float -> 6.25)
+(define (squares [xyz : (× X Y Z)] #:where (Num X) (Num Y) (Num Z)-> (× X Y Z))
+ (match2 xyz with
+ [(x,y,z) -> (tup (square x) (square y) (square z))]))
+(check-type (squares (tup 5 5 5)) : (× Int Int Int) -> (tup 25 25 25))
+(check-type (squares (tup 2.5 5 5)) : (× Float Int Int) -> (tup 6.25 25 25))
+(check-type (squares (tup 5 2.5 5)) : (× Int Float Int) -> (tup 25 6.25 25))
+(check-type (squares (tup 5 5 2.5)) : (× Int Int Float) -> (tup 25 25 6.25))
+(check-type (squares (tup 2.5 2.5 2.5)) : (× Float Float Float) -> (tup 6.25 6.25 6.25))
+(typecheck-fail (squares (tup 5 5 #f)) #:with-msg "\\(Num Bool\\) instance undefined")
+(typecheck-fail (squares (tup 5 #f 5)) #:with-msg "\\(Num Bool\\) instance undefined")
+(typecheck-fail (squares (tup #f 5 5)) #:with-msg "\\(Num Bool\\) instance undefined")
+
+;; --------------------------------------------------
+
+(define-type (TypeA X) (A [x : X] [y : X]))
+
+;; constraint of nested tyvar
+(define (test-a1 [a : (TypeA X)] #:where (Eq X) -> Bool)
+ (== (A-x a) (A-y a)))
+(check-type (test-a1 (A 1 2)) : Bool -> #f)
+(check-type (test-a1 (A "1" "2")) : Bool -> #f)
+(typecheck-fail (test-a1 (A #t #f))
+ #:with-msg
+"Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool")
+
+(define (test-a2 [a : (TypeA X)] [fa : (→ (TypeA X) X)] #:where (Eq X) -> Bool)
+ (== (fa a) (fa a)))
+
+(check-type (test-a2 (A 1 2) (inst A-x Int)) : Bool -> #t)
+(check-type (test-a2 (A "1" "2") (inst A-x String)) : Bool -> #t)
+
+(define-type (Heap X)
+ Emp
+ (H X))
+
+(define (hf [h : (Heap X)] #:where (Ord X) -> Bool)
+ (match h with
+ [Emp -> #f]
+ [H x -> (lte x x)]))
+
+(check-type (hf (H 1)) : Bool -> #t)
+(typecheck-fail (hf (H #f))
+ #:with-msg
+ "Ord Bool.*instance undefined.*Cannot instantiate function with constraints.*Ord X.*with.*X : Bool")
+
+;; type classes for non-base types
+(define-instance (Eq X) => (Eq (List X))
+ [== (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> #t]
+ [((x :: xs),(y :: ys)) -> (and (== x y) (== xs ys))]
+ [_ -> #f]))])
+
+;; nil and nil
+(check-type (== (nil {Int}) (nil {Int})) : Bool -> #t)
+;; TODO: better err msg?
+;; as of 2016-04-04: "== operation undefined for input types: Int, Bool"
+;; should somehow indicate that the two values are not equal because types differ?
+(typecheck-fail (== (nil {Int}) (nil {Bool})))
+;; nil and non-nil
+(check-type (== (nil {Int}) (list 1)) : Bool -> #f)
+(check-type (== (nil {Int}) (cons 1 nil)) : Bool -> #f)
+(check-type (== (nil {Int}) (cons 1 (cons 2 nil))) : Bool -> #f)
+;; non-nil and nil
+(check-type (== (list 1) (nil {Int})) : Bool -> #f)
+(check-type (== (cons 1 nil) (nil {Int})) : Bool -> #f)
+(check-type (== (cons 1 (cons 2 nil)) (nil {Int})) : Bool -> #f)
+;; non-nil and non-nil
+(check-type (== (list 1) (list 1)) : Bool -> #t)
+(check-type (== (cons 1 nil) (list 1)) : Bool -> #t)
+(check-type (== (list 1) (cons 1 nil)) : Bool -> #t)
+(check-type (== (list 1) (list 1 2)) : Bool -> #f)
+(check-type (== (list 1 2) (list 1)) : Bool -> #f)
+(check-type (== (list 1 2) (list 1 2)) : Bool -> #t)
+(check-type (== (list 1 2) (list 1 3)) : Bool -> #f)
+(check-type (== (list 1 3) (list 1 2)) : Bool -> #f)
+
+(define (list-eq1 [l1 : (List X)] [l2 : (List X)] #:where (Eq X) -> Bool)
+ (== l1 l2))
+
+(check-type (list-eq1 (nil {Int}) (nil {Int})) : Bool -> #t)
+(check-type (list-eq1 (nil {Int}) (list 1)) : Bool -> #f)
+(check-type (list-eq1 (list 1) (nil {Int})) : Bool -> #f)
+(check-type (list-eq1 (list 1) (list 1)) : Bool -> #t)
+(check-type (list-eq1 (list 1) (list 2)) : Bool -> #f)
+(check-type (list-eq1 (list 1) (list 1 2)) : Bool -> #f)
+
+(check-type (member? (list 1) (list (list 1))) : Bool -> #t)
+(check-type (member? (list 1) (list (list 2))) : Bool -> #f)
+(check-type (member? (list 1) (list (list 2) (list 1))) : Bool -> #t)
+
+(define (id-fn2 [xs : (List X)] #:where (Eq X) -> (List X)) xs)
+(typecheck-fail (id-fn2 (list #f)) #:with-msg "\\(Eq Bool\\) instance undefined")
+(check-type (id-fn2 (list 1)) : (List Int) -> (list 1))
+
+;; TODO: #:where TC, where TC has a tycon, like #:where (List X)
+;; still doesnt work I dont think
+#;(define (list-eq2 [l1 : (List X)] [l2 : (List X)] #:where (List X) -> Bool)
+ (== l1 l2))
+
+;; TODO: implement subclasses
+;; 2016-05-25: Done. see memsq2
+(define (memsq? [x : X] [xs : (List X)] #:where (Eq X) (Num X) -> Bool)
+ (member? (square x) xs))
+(check-type (memsq? 1 (list 1)) : Bool -> #t)
+(check-type (memsq? 2 (list 2)) : Bool -> #f)
+(check-type (memsq? 2 (list 3 4)) : Bool -> #t)
+(typecheck-fail (memsq? (list 1) (list (list 1)))
+ #:with-msg "\\(Num \\(List Int\\)\\) instance undefined")
+
+
+(define (andmap [p? : (→ X Bool)] [lst : (List X)] -> Bool)
+ (match lst with
+ [[] -> #t]
+ [x :: xs -> (and (p? x) (andmap p? xs))]))
+
+;; Set
+;; type classes for non-base types: user-defined
+(define-type (Set X) (MkSet (List X)))
+(define-instance (Eq X) => (Eq (Set X))
+ [== (λ ([s1 : (Set X)] [s2 : (Set X)])
+ (match2 (tup s1 s2) with
+ [((MkSet xs),(MkSet ys)) -> (and (andmap (λ ([y : X]) (member? y xs)) ys)
+ (andmap (λ ([x : X]) (member? x ys)) xs))]))])
+(check-type (== (MkSet (list 1)) (MkSet (list 1))) : Bool -> #t)
+(check-type (== (MkSet (list 1)) (MkSet (list 2))) : Bool -> #f)
+(check-type (== (MkSet (list 1 2)) (MkSet (list 1 2))) : Bool -> #t)
+(check-type (== (MkSet (list 1 2)) (MkSet (list 2 1))) : Bool -> #t)
+(check-type (== (MkSet (list 1 2)) (MkSet (list 1 2 3))) : Bool -> #f)
+(check-type (== (MkSet (list 3 1 2)) (MkSet (list 1 2 3))) : Bool -> #t)
+
+(check-type (member? (MkSet (list 1 2)) (list (MkSet (list 1 2)))) : Bool -> #t)
+(check-type (member? (MkSet (list 1 2)) (list (MkSet (list 1)) (MkSet (list 2 1))))
+ : Bool -> #t)
+(check-type (member? (MkSet (list "1" "2")) (list (MkSet (list "1")) (MkSet (list "2" "1"))))
+ : Bool -> #t)
+
+;; type classes for non-base types: multiple constraints
+(define-instance (Eq X) (Eq Y) => (Eq (× X Y))
+ [== (λ ([p1 : (× X Y)] [p2 : (× X Y)])
+ (match2 (tup p1 p2) with
+ [((u,v),(x,y)) -> (and (== u x) (== v y))]))])
+
+(check-type (== (tup 1 2) (tup 3 4)) : Bool -> #f)
+(check-type (== (tup 1 2) (tup 1 2)) : Bool -> #t)
+(check-type (== (tup (list 1) (list 2)) (tup (list 1) (list 2))) : Bool -> #t)
+(check-type (== (tup (list 1) (list 1 2)) (tup (list 1) (list 2 1))) : Bool -> #f)
+(check-type (== (tup (list #\a) (list #\b)) (tup (list #\a) (list #\b)))
+ : Bool -> #t)
+(check-type (== (tup (list #\a) (list #\a #\b)) (tup (list #\a) (list #\b #\a)))
+ : Bool -> #f)
+
+(check-type (== (tup (list #\a) (list 1)) (tup (list #\a) (list 1)))
+ : Bool -> #t)
+(check-type (== (tup (list #\a) (list 1 2)) (tup (list #\a) (list 2 1)))
+ : Bool -> #f)
+
+(check-type (member? (tup 1 2) (list (tup 3 4) (tup 5 6))) : Bool -> #f)
+(check-type (member? (tup 1 2) (list (tup 3 4) (tup 5 6) (tup 1 2)))
+ : Bool -> #t)
+(check-type (member? (tup 1 "2") (list (tup 3 "4") (tup 5 "6")))
+ : Bool -> #f)
+(check-type (member? (tup 1 "2") (list (tup 3 "4") (tup 5 "6") (tup 1 "2")))
+ : Bool -> #t)
+(check-type
+ (member?
+ (tup (list 1) "2")
+ (list (tup (list 3) "4") (tup (list 5) "6")))
+ : Bool -> #f)
+(check-type
+ (member?
+ (tup (list 1) "2")
+ (list (tup (list 3) "4") (tup (list 5) "6") (tup (list 1) "2")))
+ : Bool -> #t)
+
+(define-typeclass (Eq X) => (Num2 X)
+ [ad : (→ X X X)]
+ [sb : (→ X X X)]
+ [mu : (→ X X X)])
+
+(typecheck-fail
+ (define-instance (Num2 Bool)
+ [ad +] [sb -] [mu *])
+ #:with-msg "No instance defined for \\(Eq Bool\\)")
+
+(define-instance (Num2 Int)
+ [ad +] [sb -] [mu *])
+
+(define (f/sub1 [x : X] #:where (Num2 X) -> X)
+ (ad x x))
+#;(typecheck-fail ; fails
+ (define (f/sub2 [x : X] #:where (Num2 X) -> X) (== x x))
+ #:with-msg "Body has type Bool, expected/given X")
+(define (f/sub2 [x : X] #:where (Num2 X) -> Bool)
+ (== x x))
+
+(check-type f/sub1 : (=>/test (Num2 X) (→ X X)))
+(check-type f/sub2 : (=>/test (Num2 X) (→ X Bool)))
+
+(check-type (f/sub1 1) : Int -> 2)
+(typecheck-fail (f/sub1 #f) #:with-msg "\\(Num2 Bool\\) instance undefined")
+(check-type (f/sub2 1) : Bool -> #t)
+(typecheck-fail (f/sub1 #f) #:with-msg "\\(Num2 Bool\\) instance undefined")
+
+(define-instance (Num2 Float)
+ [ad fl+] [sb fl-] [mu fl*])
+
+(define (square3 [x : X] #:where (Num2 X) -> X)
+ (mu x x))
+(check-type (square3 5) : Int -> 25)
+(check-type (square3 2.5) : Float -> 6.25)
+(define (memsq2? [x : X] [xs : (List X)] #:where (Num2 X) -> Bool)
+ (member? (square3 x) xs))
+(check-type (memsq2? 1 (list 1)) : Bool -> #t)
+(check-type (memsq2? 2 (list 2)) : Bool -> #f)
+(check-type (memsq2? 2 (list 3 4)) : Bool -> #t)
+(typecheck-fail (memsq2? (list 1) (list (list 1)))
+ #:with-msg "\\(Num2 \\(List Int\\)\\) instance undefined")
+(typecheck-fail (memsq2? #f (list #f))
+ #:with-msg "\\(Num2 Bool\\) instance undefined")
+
+(define-typeclass (Top X)
+ [fun1 : (→ X X X)])
+(define-typeclass (Top X) => (Left X)
+ [fun2 : (→ X X X)])
+(define-typeclass (Top X) => (Right X)
+ [fun3 : (→ X X X)])
+(define-typeclass (Left X) (Right X) => (Bottom X)
+ [fun4 : (→ X X X)])
+
+(define-instance (Top Int)
+ [fun1 +])
+(define-instance (Left Int)
+ [fun2 +])
+(define-instance (Right Int)
+ [fun3 +])
+(define-instance (Bottom Int)
+ [fun4 +])
+(define (left-fun2 [x : X] #:where (Left X) -> X)
+ (fun2 x x))
+(check-type (left-fun2 6) : Int -> 12)
+(define (left-fun1 [x : X] #:where (Left X) -> X)
+ (fun1 x x))
+(check-type (left-fun1 6) : Int -> 12)
+(define (bott-fun4 [x : X] #:where (Bottom X) -> X)
+ (fun4 x x))
+(check-type (bott-fun4 5) : Int -> 10)
+(define (bott-fun3 [x : X] #:where (Bottom X) -> X)
+ (fun3 x x))
+(check-type (bott-fun3 5) : Int -> 10)
+(define (bott-fun2 [x : X] #:where (Bottom X) -> X)
+ (fun2 x x))
+(check-type (bott-fun2 5) : Int -> 10)
+(define (bott-fun-Int [x : Int] -> Int)
+ (fun1 x x))
+(check-type (bott-fun-Int 5) : Int -> 10)
+;; lookup more than one parent level
+(define (bott-fun1 [x : X] #:where (Bottom X) -> X)
+ (fun1 x x))
+(check-type (bott-fun1 5) : Int -> 10)
+
+;; non-base typeclass instances with subclassing
+(define-instance (Top X) => (Top (List X))
+ [fun1 (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> l2]
+ [((x :: xs),(y :: ys)) -> (cons (fun1 x y) (fun1 xs ys))]
+ [_ -> l1]))])
+(define (top-list-fun1 [xs : (List X)] #:where (Top X) -> (List X))
+ (fun1 xs xs))
+(check-type (top-list-fun1 (list 5)) : (List Int) -> (list 10))
+(check-type (top-list-fun1 (list 5 6)) : (List Int) -> (list 10 12))
+
+(define-instance (Left X) => (Left (List X))
+ [fun2 (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> l2]
+ [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun2 x1 y1) (fun2 xs1 ys1))]
+ [_ -> l1]))])
+
+(define (left-list-fun2 [zs : (List X)] #:where (Left X) -> (List X))
+ (fun2 zs zs))
+(check-type (left-list-fun2 (list 6)) : (List Int) -> (list 12))
+(define (left-list-fun1 [xx : (List X)] #:where (Left X) -> (List X))
+ (fun1 xx xx))
+(check-type (left-list-fun1 (list 6)) : (List Int) -> (list 12))
+
+;; can use fun1 (from Top), for both X and (List X),
+;; in both instance def, and regular fns
+(define-instance (Right X) => (Right (List X))
+ [fun3 (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> l2]
+ [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun1 x1 y1) (fun1 xs1 ys1))]
+ [_ -> l1]))])
+(define (right-list-fun1 [xx : (List X)] #:where (Right X) -> (List X))
+ (fun1 xx xx))
+(check-type (right-list-fun1 (list 6)) : (List Int) -> (list 12))
+
+(define-instance (Bottom X) => (Bottom (List X))
+ [fun4 (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> l2]
+ [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun4 x1 y1) (fun4 xs1 ys1))]
+ [_ -> l1]))])
+
+;; lookup more than one parent level
+(define (bott-list-fun1 [xs : (List X)] #:where (Bottom X) -> (List X))
+ (fun1 xs xs))
+(check-type (bott-list-fun1 (list 5)) : (List Int) -> (list 10))
diff --git a/macrotypes/examples/tests/run-all-mlish-tests.rkt b/macrotypes/examples/tests/run-all-mlish-tests.rkt
@@ -5,4 +5,5 @@
(do-tests "run-mlish-tests1.rkt" "General MLish"
"run-mlish-tests2.rkt" "Shootout and RW OCaml"
"run-mlish-tests3.rkt" "Ben's"
- "run-mlish-tests4.rkt" "Okasaki / polymorphic recursion")
+ "run-mlish-tests4.rkt" "Okasaki / polymorphic recursion"
+ "run-mlish-tests5.rkt" "typeclasses")
diff --git a/macrotypes/examples/tests/run-mlish-tests5.rkt b/macrotypes/examples/tests/run-mlish-tests5.rkt
@@ -0,0 +1,4 @@
+#lang racket/base
+
+;; adhoc polymorphism tests
+(require "mlish/generic.mlish")
diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt
@@ -15,6 +15,9 @@
(define (stx-flatten stxs)
(apply append (stx-map stx->list stxs)))
+(define (stx-filter p? stxs)
+ (filter p? (stx->list stxs)))
+
(define (curly-parens? stx)
(define paren-prop (syntax-property stx 'paren-shape))
(and paren-prop (char=? #\{ paren-prop)))
@@ -56,8 +59,8 @@
(define (stx-append stx1 stx2)
(append (stx->list stx1) (stx->list stx2)))
-(define (stx-appendmap f stx)
- (stx-flatten (stx-map f stx)))
+(define (stx-appendmap f . stxs)
+ (stx-flatten (apply stx-map f stxs)))
(define (stx-remove-dups Xs)
(remove-duplicates (stx->list Xs) free-identifier=?))
diff --git a/macrotypes/typecheck.rkt b/macrotypes/typecheck.rkt
@@ -392,6 +392,9 @@
(define (infer/tyctx+erase ctx e)
(syntax-parse (infer (list e) #:tvctx ctx)
[(tvs _ (e+) (τ)) (list #'tvs #'e+ #'τ)]))
+ (define (infers/tyctx+erase ctx es)
+ (syntax-parse (infer es #:tvctx ctx)
+ [(tvs+ _ es+ tys) (list #'tvs+ #'es+ #'tys)]))
; extra indirection, enables easily overriding type=? with sub?
; to add subtyping, without changing any other definitions
@@ -517,7 +520,9 @@
[(stx-pair? τ) (string-join (stx-map type->str τ)
#:before-first "("
#:after-last ")")]
- [else (format "~s" (syntax->datum τ))])))
+ [else (format "~s" (syntax->datum τ))]))
+ (define (types->str tys #:sep [sep ", "])
+ (string-join (stx-map type->str tys) sep)))
(begin-for-syntax
(define (mk-? id) (format-id id "~a?" id))
@@ -578,7 +583,15 @@
((~literal #%plain-lambda) bvs
((~literal #%expression) ((~literal quote) extra-info-macro)) . tys))
(expand/df #'(extra-info-macro . tys))]
- [_ #f])))
+ [_ #f]))
+;; gets the internal id in a type representation
+ (define (get-type-tag t)
+ (syntax-parse t
+ [((~literal #%plain-app) tycons . _) #'tycons]
+ [X:id #'X]
+ [_ (type-error #:src t #:msg "Can't get internal id: ~a" t)]))
+ (define (get-type-tags ts)
+ (stx-map get-type-tag ts)))
(define-syntax define-basic-checked-id-stx
diff --git a/turnstile/examples/mlish+adhoc.rkt b/turnstile/examples/mlish+adhoc.rkt
@@ -0,0 +1,1718 @@
+#lang s-exp "../../macrotypes/typecheck.rkt"
+(require racket/fixnum racket/flonum)
+
+(extends "ext-stlc.rkt" #:except #%app λ → + - * void = zero? sub1 add1 not let let* and #%datum begin
+ #:rename [~→ ~ext-stlc:→])
+;(reuse [inst sysf:inst] #:from "sysf.rkt")
+(require (rename-in (only-in "sysf.rkt" inst) [inst sysf:inst]))
+(provide inst)
+(require (only-in "ext-stlc.rkt" →?))
+(require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
+(reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
+(require (only-in "stlc+rec-iso.rkt" ~× ×?)) ; using current-type=? from here
+(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
+(reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
+(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list cons nil)))
+(require (only-in "stlc+cons.rkt" ~List List? List))
+(provide List)
+(reuse ref deref := Ref #:from "stlc+box.rkt")
+(require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×)
+ [tup rec] [proj get] [× ××]))
+(provide rec get ××)
+;; for pattern matching
+(require (prefix-in stlc+cons: (only-in "stlc+cons.rkt" list)))
+(require (prefix-in stlc+tup: (only-in "stlc+tup.rkt" tup)))
+
+(provide → →/test =>/test match2 define-type)
+
+(provide define-typeclass define-instance)
+
+;; ML-like language + ad-hoc polymorphism
+;; - top level recursive functions
+;; - user-definable algebraic datatypes
+;; - pattern matching
+;; - (local) type inference
+;;
+;; - type classes
+
+(define-type-constructor => #:arity > 0)
+
+;; type class helper fns
+(begin-for-syntax
+ (define (mk-app-err-msg stx #:expected [expected-τs #'()]
+ #:given [given-τs #'()]
+ #:note [note ""]
+ #:name [name #f]
+ #:action [other #f])
+ (syntax-parse stx
+ #;[(app . rst)
+ #:when (not (equal? '#%app (syntax->datum #'app)))
+ (mk-app-err-msg (syntax/loc stx (#%app app . rst))
+ #:expected expected-τs
+ #:given given-τs
+ #:note note
+ #:name name)]
+ [(app e_fn e_arg ...)
+ (define fn-name
+ (if name name
+ (format "function ~a"
+ (syntax->datum (or (get-orig #'e_fn) #'e_fn)))))
+ (define action (if other other "applying"))
+ (string-append
+ (format "~a (~a:~a):\nType error "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx))
+ action " "
+ fn-name ". " note "\n"
+ (format " Expected: ~a argument(s) with type(s): " (stx-length expected-τs))
+ (types->str expected-τs) "\n"
+ " Given:\n"
+ (string-join
+ (map (λ (e t) (format " ~a : ~a" e t)) ; indent each line
+ (syntax->datum #'(e_arg ...))
+ (if (stx-length=? #'(e_arg ...) given-τs)
+ (stx-map type->str given-τs)
+ (stx-map (lambda (e) "?") #'(e_arg ...))))
+ "\n")
+ "\n")]))
+ (define (type-hash-code tys) ; tys should be fully expanded
+ (equal-hash-code (syntax->datum (if (syntax? tys) tys #`#,tys))))
+ (define (mangle o tys)
+ (format-id o "~a~a" o (type-hash-code tys)))
+ ;; pattern expander for type class
+ (define-syntax ~TC
+ (pattern-expander
+ (syntax-parser
+ [(_ [generic-op ty-concrete-op] (~and ooo (~literal ...)))
+ #'(_ (_ (_ generic-op) ty-concrete-op) ooo)]
+ [(_ . ops+tys)
+ #:with expanded (generate-temporary)
+ #'(~and expanded
+ (~parse (_ (_ (_ gen-op) ty-op) (... ...))
+ #'expanded)
+ (~parse ops+tys #'((gen-op ty-op) (... ...))))])))
+ (define-syntax ~TC-base
+ (pattern-expander
+ (syntax-parser
+ [(_ . pat)
+ #:with expanded (generate-temporary)
+ #'(~and expanded
+ (~parse ((~TC . pat) . _) (flatten-TC #'expanded)))])))
+ (define-syntax ~TCs
+ (pattern-expander
+ (syntax-parser
+ ;; pat should be of shape ([op ty] ...)
+ [(_ pat (~and ooo (~literal ...)))
+ #:with expanded (generate-temporary)
+ ;; (stx-map (compose remove-dups flatten-TC) #'expanded)
+ ;; produces [List [List [List op+ty]]]
+ ;; - inner [List op+ty] is from the def of a TC
+ ;; - second List is from the flattened subclass TCs
+ ;; - outer List is bc this pattern matces multiple TCs
+ ;; This pattern expander collapses the inner two Lists
+ #'(~and expanded
+ (~parse (((~TC [op ty] (... ...)) (... ...)) ooo)
+ (stx-map (compose remove-dups flatten-TC) #'expanded))
+ (~parse (pat ooo) #'(([op ty] (... ...) (... ...)) ooo)))])))
+ (define (flatten-TC TC)
+ (syntax-parse TC
+ [(~=> sub-TC ... base-TC)
+ (cons #'base-TC (stx-appendmap flatten-TC #'(sub-TC ...)))]))
+ (define (remove-dups TCs)
+ (syntax-parse TCs
+ [() #'()]
+ [(TC . rst)
+ (cons #'TC (stx-filter (lambda (s) (not (typecheck? s #'TC))) (remove-dups #'rst)))])))
+;; type inference constraint solving
+(begin-for-syntax
+ ;; matching possibly polymorphic types
+ (define-syntax ~?∀
+ (pattern-expander
+ (lambda (stx)
+ (syntax-case stx ()
+ [(?∀ vars-pat body-pat)
+ #'(~or (~∀ vars-pat body-pat)
+ (~and (~not (~∀ _ _))
+ (~parse vars-pat #'())
+ body-pat))]))))
+
+ ;; type inference constraint solving
+ (define (compute-constraint τ1-τ2)
+ (syntax-parse τ1-τ2
+ [(X:id τ) #'((X τ))]
+ [((~Any tycons1 τ1 ...) (~Any tycons2 τ2 ...))
+ #:when (typecheck? #'tycons1 #'tycons2)
+ (compute-constraints #'((τ1 τ2) ...))]
+ ; should only be monomorphic?
+ [((~∀ () (~ext-stlc:→ τ1 ...)) (~∀ () (~ext-stlc:→ τ2 ...)))
+ (compute-constraints #'((τ1 τ2) ...))]
+ [_ #'()]))
+ (define (compute-constraints τs)
+ (stx-appendmap compute-constraint τs))
+
+ (define (solve-constraint x-τ)
+ (syntax-parse x-τ
+ [(X:id τ) #'((X τ))]
+ [_ #'()]))
+ (define (solve-constraints cs)
+ (stx-appendmap compute-constraint cs))
+
+ (define (lookup x substs)
+ (syntax-parse substs
+ [((y:id τ) . rst)
+ #:when (free-identifier=? #'y x)
+ #'τ]
+ [(_ . rst) (lookup x #'rst)]
+ [() #f]))
+
+ ;; find-unsolved-Xs : (Stx-Listof Id) Constraints -> (Listof Id)
+ ;; finds the free Xs that aren't constrained by cs
+ (define (find-unsolved-Xs Xs cs)
+ (for/list ([X (in-list (stx->list Xs))]
+ #:when (not (lookup X cs)))
+ X))
+
+ ;; lookup-Xs/keep-unsolved : (Stx-Listof Id) Constraints -> (Listof Type-Stx)
+ ;; looks up each X in the constraints, returning the X if it's unconstrained
+ (define (lookup-Xs/keep-unsolved Xs cs)
+ (for/list ([X (in-list (stx->list Xs))])
+ (or (lookup X cs) X)))
+
+ ;; solve for Xs by unifying quantified fn type with the concrete types of stx's args
+ ;; stx = the application stx = (#%app e_fn e_arg ...)
+ ;; tyXs = input and output types from fn type
+ ;; ie (typeof e_fn) = (-> . tyXs)
+ ;; It infers the types of arguments from left-to-right,
+ ;; and it short circuits if it's done early.
+ ;; It returns list of 3 values if successful, else throws a type error
+ ;; - a list of the arguments that it expanded
+ ;; - a list of the the un-constrained type variables
+ ;; - the constraints for substituting the types
+ (define (solve Xs tyXs stx)
+ (syntax-parse tyXs
+ [(τ_inX ... τ_outX)
+ ;; generate initial constraints with expected type and τ_outX
+ #:with expected-ty (get-expected-type stx)
+ (define initial-cs
+ (if (syntax-e #'expected-ty)
+ (compute-constraint (list #'τ_outX ((current-type-eval) #'expected-ty)))
+ #'()))
+ (syntax-parse stx
+ [(_ e_fn . args)
+ (define-values (as- cs)
+ (for/fold ([as- null] [cs initial-cs])
+ ([a (in-list (syntax->list #'args))]
+ [tyXin (in-list (syntax->list #'(τ_inX ...)))]
+ #:break (empty? (find-unsolved-Xs Xs cs)))
+ (define/with-syntax [a- ty_a] (infer+erase a))
+ (values
+ (cons #'a- as-)
+ (stx-append cs (compute-constraint (list tyXin #'ty_a))))))
+
+ (list (reverse as-) (find-unsolved-Xs Xs cs) cs)])]))
+
+ (define (raise-app-poly-infer-error stx expected-tys given-tys e_fn)
+ (type-error #:src stx
+ #:msg (mk-app-err-msg stx #:expected expected-tys #:given given-tys
+ #:note (format "Could not infer instantiation of polymorphic function ~a."
+ (syntax->datum (get-orig e_fn))))))
+
+ ;; instantiate polymorphic types
+ ;; inst-type : (Listof Type) (Listof Id) Type -> Type
+ ;; Instantiates ty with the tys-solved substituted for the Xs, where the ith
+ ;; identifier in Xs is associated with the ith type in tys-solved
+ (define (inst-type tys-solved Xs ty)
+ (substs tys-solved Xs ty))
+
+ ;; inst-type/cs : (Stx-Listof Id) Constraints Type-Stx -> Type-Stx
+ ;; Instantiates ty, substituting each identifier in Xs with its mapping in cs.
+ (define (inst-type/cs Xs cs ty)
+ (define tys-solved (lookup-Xs/keep-unsolved Xs cs))
+ (inst-type tys-solved Xs ty))
+ ;; inst-types/cs : (Stx-Listof Id) Constraints (Stx-Listof Type-Stx) -> (Listof Type-Stx)
+ ;; the plural version of inst-type/cs
+ (define (inst-types/cs Xs cs tys)
+ (stx-map (lambda (t) (inst-type/cs Xs cs t)) tys))
+
+ ;; compute unbound tyvars in one unexpanded type ty
+ (define (compute-tyvar1 ty)
+ (syntax-parse ty
+ [X:id #'(X)]
+ [() #'()]
+ [(C t ...) (stx-appendmap compute-tyvar1 #'(t ...))]))
+ ;; computes unbound ids in (unexpanded) tys, to be used as tyvars
+ (define (compute-tyvars tys)
+ (define Xs (stx-appendmap compute-tyvar1 tys))
+ (filter
+ (lambda (X)
+ (with-handlers
+ ([exn:fail:syntax:unbound? (lambda (e) #t)]
+ [exn:fail:type:infer? (lambda (e) #t)])
+ (let ([X+ ((current-type-eval) X)])
+ (not (or (tyvar? X+) (type? X+))))))
+ (stx-remove-dups Xs))))
+
+;; define --------------------------------------------------
+;; for function defs, define infers type variables
+;; - since the order of the inferred type variables depends on expansion order,
+;; which is not known to programmers, to make the result slightly more
+;; intuitive, we arbitrarily sort the inferred tyvars lexicographically
+(define-typed-syntax define/tc #:export-as define
+ [(_ x:id e)
+ #:with (e- τ) (infer+erase #'e)
+ #:with y (generate-temporary)
+ #'(begin-
+ (define-syntax- x (make-rename-transformer (⊢ y : τ)))
+ (define- y e-))]
+ ; explicit "forall"
+ [(_ Ys (f:id [x:id (~datum :) τ] ... (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e)
+ #:when (brace? #'Ys)
+ ;; TODO; remove this code duplication
+ #:with g (add-orig (generate-temporary #'f) #'f)
+ #:with e_ann (syntax/loc #'e (add-expected e τ_out))
+ #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
+ ;; TODO: check that specified return type is correct
+ ;; - currently cannot do it here; to do the check here, need all types of
+ ;; top-lvl fns, since they can call each other
+ #:with (~and ty_fn_expected (~∀ _ (~ext-stlc:→ _ ... out_expected)))
+ ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...)))
+ #`(begin-
+ (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ (define- g
+ (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]
+ ;; alternate type sig syntax, after parameter names
+ [(_ (f:id x:id ...) (~datum :) ty ... (~or (~datum ->) (~datum →)) ty_out . b)
+ (syntax/loc stx (define/tc (f [x : ty] ... -> ty_out) . b))]
+ [(_ (f:id [x:id (~datum :) τ] ... ; no TC
+ (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e)
+ #:with (~and Ys (Y ...)) (compute-tyvars #'(τ ... τ_out))
+ #:with g (add-orig (generate-temporary #'f) #'f)
+ #:with e_ann (syntax/loc #'e (add-expected e τ_out)) ; must be macro bc t_out may have unbound tvs
+ #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
+ ;; TODO: check that specified return type is correct
+ ;; - currently cannot do it here; to do the check here, need all types of
+ ;; top-lvl fns, since they can call each other
+ #:with ty_fn_expected
+ (set-stx-prop/preserved
+ ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...)))
+ 'orig
+ (list #'(→ τ+orig ...)))
+ #`(begin-
+ (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ (define- g
+ (Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))]
+ [(_ (f:id [x:id (~datum :) τ] ...
+ (~seq #:where TC ...)
+ (~or (~datum ->) (~datum →)) τ_out)
+ e_body ... e)
+ #:with (~and Ys (Y ...)) (compute-tyvars #'(τ ... τ_out))
+ #:with g (add-orig (generate-temporary #'f) #'f)
+ #:with e_ann (syntax/loc #'e (add-expected e τ_out)) ; must be macro bc t_out may have unbound tvs
+ #:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
+ ;; TODO: check that specified return type is correct
+ ;; - currently cannot do it here; to do the check here, need all types of
+ ;; top-lvl fns, since they can call each other
+ #:with (~and ty_fn_expected (~∀ _ (~=> _ ... (~ext-stlc:→ _ ... out_expected))))
+ (syntax-property
+ ((current-type-eval) #'(∀ Ys (=> TC ... (ext-stlc:→ τ+orig ...))))
+ 'orig
+ (list #'(→ τ+orig ...)))
+ #`(begin-
+ (define-syntax- f (make-rename-transformer (⊢ g : ty_fn_expected)))
+ #,(quasisyntax/loc stx
+ (define- g
+ ;(Λ Ys (ext-stlc:λ ([x : τ] ...) (ext-stlc:begin e_body ... e_ann)))))])
+ (liftedλ {Y ...} ([x : τ] ... #:where TC ...)
+ #,(syntax/loc #'e_ann (ext-stlc:begin e_body ... e_ann))))))])
+
+;; define-type -----------------------------------------------
+;; TODO: should validate τ as part of define-type definition (before it's used)
+;; - not completely possible, since some constructors may not be defined yet,
+;; ie, mutually recursive datatypes
+;; for now, validate types but punt if encountering unbound ids
+(define-syntax (define-type stx)
+ (syntax-parse stx
+ [(_ Name:id . rst)
+ #:with NewName (generate-temporary #'Name)
+ #:with Name2 (add-orig #'(NewName) #'Name)
+ #`(begin-
+ (define-type Name2 . #,(subst #'Name2 #'Name #'rst))
+ (stlc+rec-iso:define-type-alias Name Name2))]
+ [(_ (Name:id X:id ...)
+ ;; constructors must have the form (Cons τ ...)
+ ;; but the first ~or clause accepts 0-arg constructors as ids;
+ ;; the ~and is a workaround to bind the duplicate Cons ids (see Ryan's email)
+ (~and (~or (~and IdCons:id
+ (~parse (Cons [fld (~datum :) τ] ...) #'(IdCons)))
+ (Cons [fld (~datum :) τ] ...)
+ (~and (Cons τ ...)
+ (~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
+ ;; validate tys
+ #:with (ty_flat ...) (stx-flatten #'((τ ...) ...))
+ #:with (_ _ (_ _ (_ _ (_ _ ty+ ...))))
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (λ (e)
+ (define X (stx-car (exn:fail:syntax-exprs e)))
+ #`(lambda () (let-syntax () (let-syntax () (#%app void unbound)))))])
+ (expand/df
+ #`(lambda (X ...)
+ (let-syntax
+ ([Name
+ (syntax-parser
+ [(_ X ...) (mk-type #'void)]
+ [stx
+ (type-error
+ #:src #'stx
+ #:msg
+ (format "Improper use of constructor ~a; expected ~a args, got ~a"
+ (syntax->datum #'Name) (stx-length #'(X ...))
+ (stx-length (stx-cdr #'stx))))])]
+ [X (make-rename-transformer (⊢ X #%type))] ...)
+ (void ty_flat ...)))))
+ #:when (or (equal? '(unbound) (syntax->datum #'(ty+ ...)))
+ (stx-map
+ (lambda (t+ t) (unless (type? t+)
+ (type-error #:src t
+ #:msg "~a is not a valid type" t)))
+ #'(ty+ ...) #'(ty_flat ...)))
+ #:with NameExpander (format-id #'Name "~~~a" #'Name)
+ #:with NameExtraInfo (format-id #'Name "~a-extra-info" #'Name)
+ #:with (StructName ...) (generate-temporaries #'(Cons ...))
+ #:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
+ #:with ((exposed-acc ...) ...)
+ (stx-map
+ (λ (C fs) (stx-map (λ (f) (format-id C "~a-~a" C f)) fs))
+ #'(Cons ...) #'((fld ...) ...))
+ #:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
+ #'(StructName ...) #'((fld ...) ...))
+ #:with (Cons? ...) (stx-map mk-? #'(StructName ...))
+ #:with (exposed-Cons? ...) (stx-map mk-? #'(Cons ...))
+ #`(begin-
+ (define-syntax- (NameExtraInfo stx)
+ (syntax-parse stx
+ [(_ X ...) #'(('Cons 'StructName Cons? [acc τ] ...) ...)]))
+ (define-type-constructor Name
+ #:arity = #,(stx-length #'(X ...))
+ #:extra-info 'NameExtraInfo
+ #:no-provide)
+ (struct- StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
+ (define-syntax- (exposed-acc stx) ; accessor for records
+ (syntax-parse stx
+ [_:id (⊢ acc (∀ (X ...) (ext-stlc:→ (Name X ...) τ)))]
+ [(o . rst) ; handle if used in fn position
+ #:with app (datum->syntax #'o '#%app)
+ #`(app
+ #,(assign-type #'acc #'(∀ (X ...) (ext-stlc:→ (Name X ...) τ)))
+ . rst)])) ... ...
+ (define-syntax- (exposed-Cons? stx) ; predicates for each variant
+ (syntax-parse stx
+ [_:id (⊢ Cons? (∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))]
+ [(o . rst) ; handle if used in fn position
+ #:with app (datum->syntax #'o '#%app)
+ #`(app
+ #,(assign-type #'Cons? #'(∀ (X ...) (ext-stlc:→ (Name X ...) Bool)))
+ . rst)])) ...
+ (define-syntax- (Cons stx)
+ (syntax-parse stx
+ ; no args and not polymorphic
+ [C:id #:when (and (stx-null? #'(X ...)) (stx-null? #'(τ ...))) #'(C)]
+ ; no args but polymorphic, check inferred type
+ [C:id
+ #:when (stx-null? #'(τ ...))
+ #:with τ-expected (syntax-property #'C 'expected-type)
+ #:fail-unless (syntax-e #'τ-expected)
+ (raise
+ (exn:fail:type:infer
+ (string-append
+ (format "TYPE-ERROR: ~a (~a:~a): "
+ (syntax-source stx) (syntax-line stx) (syntax-column stx))
+ (format "cannot infer type of ~a; add annotations"
+ (syntax->datum #'C)))
+ (current-continuation-marks)))
+ #:with (NameExpander τ-expected-arg (... ...)) ((current-type-eval) #'τ-expected)
+ #'(C {τ-expected-arg (... ...)})]
+ [_:id (⊢ StructName (∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))] ; HO fn
+ [(C τs e_arg ...)
+ #:when (brace? #'τs) ; commit to this clause
+ #:with {~! τ_X:type (... ...)} #'τs
+ #:with (τ_in:type (... ...)) ; instantiated types
+ (stx-map
+ (λ (t) (substs #'(τ_X.norm (... ...)) #'(X ...) t))
+ #'(τ ...))
+ #:with ([e_arg- τ_arg] ...)
+ (stx-map
+ (λ (e τ_e)
+ (infer+erase (set-stx-prop/preserved e 'expected-type τ_e)))
+ #'(e_arg ...) #'(τ_in.norm (... ...)))
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in.norm (... ...)))
+ (mk-app-err-msg (syntax/loc stx (#%app C e_arg ...))
+ #:expected #'(τ_in.norm (... ...)) #:given #'(τ_arg ...)
+ #:name (format "constructor ~a" 'Cons))
+ (⊢ (StructName e_arg- ...) : (Name τ_X (... ...)))]
+ [(C . args) ; no type annotations, must infer instantiation
+ #:with StructName/ty
+ (set-stx-prop/preserved
+ (⊢ StructName : (∀ (X ...) (ext-stlc:→ τ ... (Name X ...))))
+ 'orig
+ (list #'C))
+ ; stx/loc transfers expected-type
+ (syntax/loc stx (mlish:#%app StructName/ty . args))]))
+ ...)]))
+
+;; match --------------------------------------------------
+(begin-for-syntax
+ (define (get-ctx pat ty)
+ (unify-pat+ty (list pat ty)))
+ (define (unify-pat+ty pat+ty)
+ (syntax-parse pat+ty
+ [(pat ty) #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
+ (syntax-parse #'pat
+ [{(~datum _)} #'()]
+ [{(~literal stlc+cons:nil)} #'()]
+ [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
+ #:when (get-extra-info #'ty)
+ #'()]
+ ;; comma tup syntax always has parens
+ [{(~and ps (p1 (unq p) ...))}
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ (unify-pat+ty #'(ps ty))]
+ [{p ...}
+ (unify-pat+ty #'((p ...) ty))])] ; pair
+ [((~datum _) ty) #'()]
+ [((~or (~literal stlc+cons:nil)) ty) #'()]
+ [(A:id ty) ; disambiguate 0-arity constructors (that don't need parens)
+ #:with (_ (_ (_ C) . _) ...) (get-extra-info #'ty)
+ #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
+ #'()]
+ [(x:id ty) #'((x ty))]
+ [((p1 (unq p) ...) ty) ; comma tup stx
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ #:with (~× t ...) #'ty
+ #:with (pp ...) #'(p1 p ...)
+ (unifys #'([pp t] ...))]
+ [(((~literal stlc+tup:tup) p ...) ty) ; tup
+ #:with (~× t ...) #'ty
+ (unifys #'([p t] ...))]
+ [(((~literal stlc+cons:list) p ...) ty) ; known length list
+ #:with (~List t) #'ty
+ (unifys #'([p t] ...))]
+ [(((~seq p (~datum ::)) ... rst) ty) ; nicer cons stx
+ #:with (~List t) #'ty
+ (unifys #'([p t] ... [rst ty]))]
+ [(((~literal stlc+cons:cons) p ps) ty) ; arb length list
+ #:with (~List t) #'ty
+ (unifys #'([p t] [ps ty]))]
+ [((Name p ...) ty)
+ #:with (_ (_ Cons) _ _ [_ _ τ] ...)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst)
+ (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+ (stx-cdr (get-extra-info #'ty)))
+ (unifys #'([p τ] ...))]
+ [p+t #:fail-when #t (format "could not unify ~a" (syntax->datum #'p+t))
+ #'()]))
+ (define (unifys p+tys) (stx-appendmap unify-pat+ty p+tys))
+
+ (define (compile-pat p ty)
+ (syntax-parse p
+ [pat #:when (brace? #'pat) ; handle root pattern specially (to avoid some parens)
+ (syntax-parse #'pat
+ [{(~datum _)} #'_]
+ [{(~literal stlc+cons:nil)} (syntax/loc p (list))]
+ [{A:id} ; disambiguate 0-arity constructors (that don't need parens)
+ #:when (get-extra-info ty)
+ (compile-pat #'(A) ty)]
+ ;; comma tup stx always has parens
+ [{(~and ps (p1 (unq p) ...))}
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ (compile-pat #'ps ty)]
+ [{pat ...} (compile-pat (syntax/loc p (pat ...)) ty)])]
+ [(~datum _) #'_]
+ [(~literal stlc+cons:nil) ; nil
+ #'(list)]
+ [A:id ; disambiguate 0-arity constructors (that don't need parens)
+ #:with (_ (_ (_ C) . _) ...) (get-extra-info ty)
+ #:when (member (syntax->datum #'A) (syntax->datum #'(C ...)))
+ (compile-pat #'(A) ty)]
+ [x:id p]
+ [(p1 (unq p) ...) ; comma tup stx
+ #:when (not (stx-null? #'(p ...)))
+ #:when (andmap (lambda (u) (equal? u 'unquote)) (syntax->datum #'(unq ...)))
+ #:with (~× t ...) ty
+ #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'(p1 p ...) #'(t ...))
+ #'(list p- ...)]
+ [((~literal stlc+tup:tup) . pats)
+ #:with (~× . tys) ty
+ #:with (p- ...) (stx-map (lambda (p t) (compile-pat p t)) #'pats #'tys)
+ (syntax/loc p (list p- ...))]
+ [((~literal stlc+cons:list) . ps)
+ #:with (~List t) ty
+ #:with (p- ...) (stx-map (lambda (p) (compile-pat p #'t)) #'ps)
+ (syntax/loc p (list p- ...))]
+ [((~seq pat (~datum ::)) ... last) ; nicer cons stx
+ #:with (~List t) ty
+ #:with (p- ...) (stx-map (lambda (pp) (compile-pat pp #'t)) #'(pat ...))
+ #:with last- (compile-pat #'last ty)
+ (syntax/loc p (list-rest p- ... last-))]
+ [((~literal stlc+cons:cons) p ps)
+ #:with (~List t) ty
+ #:with p- (compile-pat #'p #'t)
+ #:with ps- (compile-pat #'ps ty)
+ #'(cons p- ps-)]
+ [(Name . pats)
+ #:with (_ (_ Cons) (_ StructName) _ [_ _ τ] ...)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst)
+ (equal? (syntax->datum #'Name) (syntax->datum #'C))])
+ (stx-cdr (get-extra-info ty)))
+ #:with (p- ...) (stx-map compile-pat #'pats #'(τ ...))
+ (syntax/loc p (StructName p- ...))]))
+
+ ;; pats = compiled pats = racket pats
+ (define (check-exhaust pats ty)
+ (define (else-pat? p)
+ (syntax-parse p [(~literal _) #t] [_ #f]))
+ (define (nil-pat? p)
+ (syntax-parse p
+ [((~literal list)) #t]
+ [_ #f]))
+ (define (non-nil-pat? p)
+ (syntax-parse p
+ [((~literal list-rest) . rst) #t]
+ [((~literal cons) . rst) #t]
+ [_ #f]))
+ (define (tup-pat? p)
+ (syntax-parse p
+ [((~literal list) . _) #t] [_ #f]))
+ (cond
+ [(or (stx-ormap else-pat? pats) (stx-ormap identifier? pats)) #t]
+ [(List? ty) ; lists
+ (unless (stx-ormap nil-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing nil clause for list expression"
+ (syntax-line last) (syntax-column last)))))
+ (unless (stx-ormap non-nil-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing clause for non-empty, arbitrary length list"
+ (syntax-line last) (syntax-column last)))))
+ #t]
+ [(×? ty) ; tuples
+ (unless (stx-ormap tup-pat? pats)
+ (error 'match2 (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) missing pattern for tuple expression"
+ (syntax-line last) (syntax-column last)))))
+ (syntax-parse pats
+ [((_ p ...) ...)
+ (syntax-parse ty
+ [(~× t ...)
+ (apply stx-andmap
+ (lambda (t . ps) (check-exhaust ps t))
+ #'(t ...)
+ (syntax->list #'((p ...) ...)))])])]
+ [else ; algebraic datatypes
+ (syntax-parse (get-extra-info ty)
+ [(_ (_ (_ C) (_ Cstruct) . rst) ...)
+ (syntax-parse pats
+ [((Cpat _ ...) ...)
+ (define Cs (syntax->datum #'(C ...)))
+ (define Cstructs (syntax->datum #'(Cstruct ...)))
+ (define Cpats (syntax->datum #'(Cpat ...)))
+ (unless (set=? Cstructs Cpats)
+ (error 'match2
+ (let ([last (car (stx-rev pats))])
+ (format "(~a:~a) clauses not exhaustive; missing: ~a"
+ (syntax-line last) (syntax-column last)
+ (string-join
+ (for/list ([C Cs][Cstr Cstructs] #:unless (member Cstr Cpats))
+ (symbol->string C))
+ ", ")))))
+ #t])]
+ [_ #t])]))
+
+ ;; TODO: do get-ctx and compile-pat in one pass
+ (define (compile-pats pats ty)
+ (stx-map (lambda (p) (list (get-ctx p ty) (compile-pat p ty))) pats))
+ )
+
+(define-syntax (match2 stx)
+ (syntax-parse stx #:datum-literals (with)
+ [(_ e with . clauses)
+ #:fail-when (null? (syntax->list #'clauses)) "no clauses"
+ #:with [e- τ_e] (infer+erase #'e)
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([(~seq p ...) -> e_body] ...)
+ #:with (pat ...) (stx-map ; use brace to indicate root pattern
+ (lambda (ps) (syntax-parse ps [(pp ...) (syntax/loc stx {pp ...})]))
+ #'((p ...) ...))
+ #:with ([(~and ctx ([x ty] ...)) pat-] ...) (compile-pats #'(pat ...) #'τ_e)
+ #:with ty-expected (get-expected-type stx)
+ #:with ([(x- ...) e_body- ty_body] ...)
+ (stx-map
+ infer/ctx+erase
+ #'(ctx ...) #'((add-expected e_body ty-expected) ...))
+ #:when (check-exhaust #'(pat- ...) #'τ_e)
+ #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
+ (⊢ (match- e- [pat- (let- ([x- x] ...) e_body-)] ...) : τ_out)
+ ])]))
+
+(define-typed-syntax match #:datum-literals (with)
+ [(_ e with . clauses)
+ #:fail-when (null? (syntax->list #'clauses)) "no clauses"
+ #:with [e- τ_e] (infer+erase #'e)
+ #:with t_expect (syntax-property stx 'expected-type) ; propagate inferred type
+ (cond
+ [(×? #'τ_e) ;; e is tuple
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([x ... -> e_body])
+ #:with (~× ty ...) #'τ_e
+ #:fail-unless (stx-length=? #'(ty ...) #'(x ...))
+ "match clause pattern not compatible with given tuple"
+ #:with [(x- ...) e_body- ty_body] (infer/ctx+erase #'([x ty] ...)
+ #'(add-expected e_body t_expect))
+ #:with (acc ...) (for/list ([(a i) (in-indexed (syntax->list #'(x ...)))])
+ #`(lambda (s) (list-ref s #,(datum->syntax #'here i))))
+ #:with z (generate-temporary)
+ (⊢ (let- ([z e-])
+ (let- ([x- (acc z)] ...) e_body-))
+ : ty_body)])]
+ [(List? #'τ_e) ;; e is List
+ (syntax-parse #'clauses #:datum-literals (-> ::)
+ [([(~or (~and (~and xs [x ...]) (~parse rst (generate-temporary)))
+ (~and (~seq (~seq x ::) ... rst:id) (~parse xs #'())))
+ -> e_body] ...+)
+ #:fail-unless (stx-ormap
+ (lambda (xx) (and (brack? xx) (zero? (stx-length xx))))
+ #'(xs ...))
+ "match: missing empty list case"
+ #:fail-when (and (stx-andmap brack? #'(xs ...))
+ (= 1 (stx-length #'(xs ...))))
+ "match: missing non-empty list case"
+ #:with (~List ty) #'τ_e
+ #:with ([(x- ... rst-) e_body- ty_body] ...)
+ (stx-map (lambda (ctx e) (infer/ctx+erase ctx e))
+ #'(([x ty] ... [rst (List ty)]) ...) #'((add-expected e_body t_expect) ...))
+ #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
+ #:with (len ...) (stx-map (lambda (p) #`#,(stx-length p)) #'((x ...) ...))
+ #:with (lenop ...) (stx-map (lambda (p) (if (brack? p) #'=- #'>=-)) #'(xs ...))
+ #:with (pred? ...) (stx-map
+ (lambda (l lo) #`(λ- (lst) (#,lo (length- lst) #,l)))
+ #'(len ...) #'(lenop ...))
+ #:with ((acc1 ...) ...) (stx-map
+ (lambda (xs)
+ (for/list ([(x i) (in-indexed (syntax->list xs))])
+ #`(lambda (lst) (list-ref lst #,(datum->syntax #'here i)))))
+ #'((x ...) ...))
+ #:with (acc2 ...) (stx-map (lambda (l) #`(lambda (lst) (list-tail lst #,l))) #'(len ...))
+ (⊢ (let- ([z e-])
+ (cond-
+ [(pred? z)
+ (let- ([x- (acc1 z)] ... [rst- (acc2 z)]) e_body-)] ...))
+ : τ_out)])]
+ [else ;; e is variant
+ (syntax-parse #'clauses #:datum-literals (->)
+ [([Clause:id x:id ...
+ (~optional (~seq #:when e_guard) #:defaults ([e_guard #'(ext-stlc:#%datum . #t)]))
+ -> e_c_un] ...+) ; un = unannotated with expected ty
+ ;; length #'clauses may be > length #'info, due to guards
+ #:with info-body (get-extra-info #'τ_e)
+ #:with (_ (_ (_ ConsAll) . _) ...) #'info-body
+ #:fail-unless (set=? (syntax->datum #'(Clause ...))
+ (syntax->datum #'(ConsAll ...)))
+ (type-error #:src stx
+ #:msg (string-append
+ "match: clauses not exhaustive; missing: "
+ (string-join
+ (map symbol->string
+ (set-subtract
+ (syntax->datum #'(ConsAll ...))
+ (syntax->datum #'(Clause ...))))
+ ", ")))
+ #:with ((_ _ _ Cons? [_ acc τ] ...) ...)
+ (map ; ok to compare symbols since clause names can't be rebound
+ (lambda (Cl)
+ (stx-findf
+ (syntax-parser
+ [(_ 'C . rst) (equal? Cl (syntax->datum #'C))])
+ (stx-cdr #'info-body))) ; drop leading #%app
+ (syntax->datum #'(Clause ...)))
+ ;; this commented block experiments with expanding to unsafe ops
+ ;; #:with ((acc ...) ...) (stx-map
+ ;; (lambda (accs)
+ ;; (for/list ([(a i) (in-indexed (syntax->list accs))])
+ ;; #`(lambda (s) (unsafe-struct*-ref s #,(datum->syntax #'here i)))))
+ ;; #'((acc-fn ...) ...))
+ #:with (e_c ...+) (stx-map (lambda (ec) (add-expected-ty ec #'t_expect)) #'(e_c_un ...))
+ #:with (((x- ...) (e_guard- e_c-) (τ_guard τ_ec)) ...)
+ (stx-map
+ (λ (bs eg+ec) (infers/ctx+erase bs eg+ec))
+ #'(([x : τ] ...) ...) #'((e_guard e_c) ...))
+ #:fail-unless (and (same-types? #'(τ_guard ...))
+ (Bool? (stx-car #'(τ_guard ...))))
+ "guard expression(s) must have type bool"
+ #:with τ_out (stx-foldr (current-join) (stx-car #'(τ_ec ...)) (stx-cdr #'(τ_ec ...)))
+ #:with z (generate-temporary) ; dont duplicate eval of test expr
+ (⊢ (let- ([z e-])
+ (cond-
+ [(and- (Cons? z)
+ (let- ([x- (acc z)] ...) e_guard-))
+ (let- ([x- (acc z)] ...) e_c-)] ...))
+ : τ_out)])])])
+
+(define-syntax → ; wrapping →
+ (syntax-parser
+ [(_ ty ... #:TC TC ...)
+ #'(∀ () (=> TC ... (ext-stlc:→ ty ...)))]
+ [(_ Xs . rst)
+ #:when (brace? #'Xs)
+ #:with (X ...) #'Xs
+ (syntax-property
+ #'(∀ (X ...) (ext-stlc:→ . rst))
+ 'orig (list #'(→ . rst)))]
+ [(_ . rst) (set-stx-prop/preserved #'(∀ () (ext-stlc:→ . rst)) 'orig (list #'(→ . rst)))]))
+; special arrow that computes free vars; for use with tests
+; (because we can't write explicit forall
+(define-syntax →/test
+ (syntax-parser
+ [(_ (~and Xs (X:id ...)) . rst)
+ #:when (brace? #'Xs)
+ #'(∀ (X ...) (ext-stlc:→ . rst))]
+ [(_ . rst)
+ #:with Xs (compute-tyvars #'rst)
+ #'(∀ Xs (ext-stlc:→ . rst))]))
+
+(define-syntax =>/test
+ (syntax-parser
+ [(_ . (~and rst (TC ... (_arr . tys_arr))))
+ #:with Xs (compute-tyvars #'rst)
+ #'(∀ Xs (=> TC ... (ext-stlc:→ . tys_arr)))]))
+
+; redefine these to use lifted →
+(define-primop + : (→ Int Int Int))
+(define-primop - : (→ Int Int Int))
+(define-primop * : (→ Int Int Int))
+(define-primop max : (→ Int Int Int))
+(define-primop min : (→ Int Int Int))
+(define-primop void : (→ Unit))
+(define-primop = : (→ Int Int Bool))
+(define-primop <= : (→ Int Int Bool))
+(define-primop >= : (→ Int Int Bool))
+(define-primop < : (→ Int Int Bool))
+(define-primop > : (→ Int Int Bool))
+(define-primop modulo : (→ Int Int Int))
+(define-primop zero? : (→ Int Bool))
+(define-primop sub1 : (→ Int Int))
+(define-primop add1 : (→ Int Int))
+(define-primop not : (→ Bool Bool))
+(define-primop abs : (→ Int Int))
+(define-primop even? : (→ Int Bool))
+(define-primop odd? : (→ Int Bool))
+
+;; λ --------------------------------------------------------------------------
+
+; all λs have type (∀ (X ...) (→ τ_in ... τ_out)), even monomorphic fns
+(define-typed-syntax liftedλ #:export-as λ
+ [(_ ([x:id (~datum :) ty] ... #:where TC ...) body)
+ #:with (X ...) (compute-tyvars #'(ty ...))
+ (syntax/loc stx (liftedλ {X ...} ([x : ty] ... #:where TC ...) body))]
+ ;; TODO: I dont think this works for nested lambdas
+ ;; ie, this will will re-infer tyvars X that should be bound by outer lam
+ ;; - tyvars need to be bound in 2nd expand/df
+ ;; - This is fixed in master by Alex
+ [(_ (~and Xs (X ...)) ([x:id (~datum :) ty] ... #:where TC ...) body)
+ #:when (brace? #'Xs)
+ #:with (_ Xs+
+ (_ () (_ () (_ () (_ () ; 2 let-stx = 4 let-values
+ (_ (_ _ TC+ ...)
+ (_ _ ty+ ...)
+ (_ op-tmps+
+ (_ () (_ ()
+ ((~literal #%expression)
+ (_ xs+
+ (_ () (_ () body+)))))))))))))
+ (expand/df
+ #'(lambda (X ...)
+ (let-syntax
+ ([X (make-rename-transformer (assign-type #'X #'#%type))] ...)
+ (let-syntax
+ ;; must have this inner macro bc body of lambda may require
+ ;; ops defined by TC to be bound
+ ([a (syntax-parser [(_)
+ (syntax-parse (expand/df #'(void TC ...)) ; must expand in ctx of Xs
+ [(_ _ .
+ (~and (TC+ (... ...))
+ (~TCs ([op-sym ty-op] (... ...)) (... ...))))
+ ;; here, * suffix = flattened list
+ ;; op* ... = op-sym ... with proper ctx, and then flattened
+ #:with (op* (... ...))
+ (stx-appendmap
+ (lambda (os tc)
+ (stx-map (lambda (o) (format-id tc "~a" o)) os))
+ #'((op-sym (... ...)) (... ...)) #'(TC ...))
+ #:with (op-tmp* (... ...)) (generate-temporaries #'(op* (... ...)))
+ #:with (ty-op* (... ...)) (stx-flatten #'((ty-op (... ...)) (... ...)))
+ #:with ty-in-tagsss
+ (stx-map
+ (syntax-parser
+ [(~∀ _ fa-body)
+ (get-type-tags
+ (syntax-parse #'fa-body
+ [(~ext-stlc:→ in (... ...) _) #'(in (... ...))]
+ [(~=> _ (... ...) (~ext-stlc:→ in (... ...) _)) #'(in (... ...))]))])
+ #'(ty-op* (... ...)))
+ #:with (mangled-op (... ...)) (stx-map mangle #'(op* (... ...)) #'ty-in-tagsss)
+ #:with (y (... ...)) #'(x ...)
+ #:with (_ _ ty+ (... ...)) (expand/df #'(void ty ...))
+ #:with res
+ (expand/df
+ #'(lambda (op-tmp* (... ...))
+ (let-syntax
+ ([mangled-op
+ (make-rename-transformer (assign-type #'op-tmp* #'ty-op*))] (... ...))
+ (lambda (y (... ...))
+ (let-syntax
+ ([y (make-rename-transformer (assign-type #'y #'ty+))] (... ...))
+ body)))))
+ #'((void TC+ (... ...)) (void ty+ (... ...)) res)])])])
+ (a)))))
+ #:with ty-out (typeof #'body+)
+ #:with ty-out-expected (get-expected-type #'body+)
+ #:fail-unless (or (not (syntax-e #'ty-out-expected))
+ (typecheck? #'ty-out #'ty-out-expected))
+ (type-error #:src #'body
+ #:msg "Body has type ~a, expected/given: ~a"
+ #'ty-out #'ty-out-expected)
+ (⊢ (λ op-tmps+ (λ xs+ body+))
+ : (∀ Xs+ (=> TC+ ... (ext-stlc:→ ty+ ... ty-out))))]
+ [(_ ([x:id (~datum :) ty] ...) body) ; no TC
+ #:with (X ...) (compute-tyvars #'(ty ...))
+ #:with (~∀ () (~ext-stlc:→ _ ... body-ty)) (get-expected-type stx)
+ #'(Λ (X ...) (ext-stlc:λ ([x : ty] ...) (add-expected body body-ty)))]
+ [(_ ([x:id (~datum :) ty] ...) body) ; no TC, ignoring expected-type
+ #:with (X ...) (compute-tyvars #'(ty ...))
+ #'(Λ (X ...) (ext-stlc:λ ([x : ty] ...) body))]
+ [(_ (x:id ...+) body)
+ #:with (~?∀ Xs expected) (get-expected-type stx)
+ #:do [(unless (→? #'expected)
+ (type-error #:src stx #:msg "λ parameters must have type annotations"))]
+ #:with (~ext-stlc:→ arg-ty ... body-ty) #'expected
+ #:do [(unless (stx-length=? #'[x ...] #'[arg-ty ...])
+ (type-error #:src stx #:msg
+ (format "expected a function of ~a arguments, got one with ~a arguments"
+ (stx-length #'[arg-ty ...] #'[x ...]))))]
+ #`(Λ Xs (ext-stlc:λ ([x : arg-ty] ...) #,(add-expected-ty #'body #'body-ty)))]
+ #;[(_ args body)
+ #:with (~∀ () (~ext-stlc:→ arg-ty ... body-ty)) (get-expected-type stx)
+ #`(Λ () (ext-stlc:λ args #,(add-expected-ty #'body #'body-ty)))]
+ #;[(_ (~and x+tys ([_ (~datum :) ty] ...)) . body)
+ #:with Xs (compute-tyvars #'(ty ...))
+ ;; TODO is there a way to have λs that refer to ids defined after them?
+ #'(Λ Xs (ext-stlc:λ x+tys . body))])
+
+
+;; #%app --------------------------------------------------
+(define-typed-syntax mlish:#%app #:export-as #%app
+ [(_ e_fn . e_args)
+; #:when (printf "app: ~a\n" (syntax->datum #'(e_fn . e_args)))
+ ;; ) compute fn type (ie ∀ and →)
+ #:with [e_fn- (~and ty_fn (~∀ Xs ty_fnX))] (infer+erase #'e_fn)
+ (cond
+ [(stx-null? #'Xs)
+ (define/with-syntax tyX_args
+ (syntax-parse #'ty_fnX
+ [(~ext-stlc:→ . tyX_args) #'tyX_args]))
+ (syntax-parse #'(e_args tyX_args)
+ [((e_arg ...) (τ_inX ... _))
+ #:fail-unless (stx-length=? #'(e_arg ...) #'(τ_inX ...))
+ (mk-app-err-msg stx #:expected #'(τ_inX ...)
+ #:note "Wrong number of arguments.")
+ #:with e_fn/ty (⊢ e_fn- : (ext-stlc:→ . tyX_args))
+ #'(ext-stlc:#%app e_fn/ty (add-expected e_arg τ_inX) ...)])]
+ [else
+ (syntax-parse #'ty_fnX
+ ;; TODO: combine these two clauses
+ ;; no typeclasses, duplicate code for now --------------------------------
+ [(~ext-stlc:→ . tyX_args)
+ ;; ) solve for type variables Xs
+ (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args stx))
+ ;; ) instantiate polymorphic function type
+ (syntax-parse (inst-types/cs #'Xs #'cs #'tyX_args)
+ [(τ_in ... τ_out) ; concrete types
+ ;; ) arity check
+ #:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
+ (mk-app-err-msg stx #:expected #'(τ_in ...)
+ #:note "Wrong number of arguments.")
+ ;; ) compute argument types; re-use args expanded during solve
+ #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))])
+ (infers+erase
+ (stx-map add-expected-ty
+ (stx-drop #'e_args n) (stx-drop #'(τ_in ...) n))))
+ #:with (τ_arg1 ...) (stx-map typeof #'(e_arg1- ...))
+ #:with (τ_arg ...) #'(τ_arg1 ... τ_arg2 ...)
+ #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...)
+ ;; ) typecheck args
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+ (mk-app-err-msg stx
+ #:given #'(τ_arg ...)
+ #:expected
+ (stx-map
+ (lambda (tyin)
+ (define old-orig (get-orig tyin))
+ (define new-orig
+ (and old-orig
+ (substs
+ (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig
+ (lambda (x y)
+ (equal? (syntax->datum x) (syntax->datum y))))))
+ (syntax-property tyin 'orig (list new-orig)))
+ #'(τ_in ...)))
+ #:with τ_out* (if (stx-null? #'(unsolved-X ...))
+ #'τ_out
+ (syntax-parse #'τ_out
+ [(~?∀ (Y ...) τ_out)
+ (unless (→? #'τ_out)
+ (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
+ #'(∀ (unsolved-X ... Y ...) τ_out)]))
+ (⊢ (#%app- e_fn- e_arg- ...) : τ_out*)])]
+ ;; handle type class constraints ----------------------------------------
+ [(~=> TCX ... (~ext-stlc:→ . tyX_args))
+ ;; ) solve for type variables Xs
+ (define/with-syntax ((e_arg1- ...) (unsolved-X ...) cs) (solve #'Xs #'tyX_args stx))
+ ;; ) instantiate polymorphic function type
+ (syntax-parse (inst-types/cs #'Xs #'cs #'((TCX ...) tyX_args))
+ [((TC ...) (τ_in ... τ_out)) ; concrete types
+ #:with (~TCs ([generic-op ty-concrete-op] ...) ...) #'(TC ...)
+ #:with (op ...)
+ (stx-appendmap
+ (lambda (gen-ops conc-op-tys TC)
+ (map
+ (lambda (o tys)
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (lambda (e)
+ (type-error #:src stx
+ #:msg
+ (format
+ (string-append
+ "~a instance undefined. "
+ "Cannot instantiate function with constraints "
+ "~a with:\n ~a")
+ (type->str
+ (let*
+ ([old-orig (get-orig TC)]
+ [new-orig
+ (and
+ old-orig
+ (substs (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig
+ (lambda (x y)
+ (equal? (syntax->datum x)
+ (syntax->datum y)))))])
+ (syntax-property TC 'orig (list new-orig))))
+ (types->str #'(TCX ...))
+ (string-join
+ (stx-map
+ (lambda (X ty-solved)
+ (string-append (type->str X) " : " (type->str ty-solved)))
+ #'Xs (lookup-Xs/keep-unsolved #'Xs #'cs)) ", "))))])
+ (lookup-op o tys)))
+ (stx-map (lambda (o) (format-id stx "~a" o #:source stx)) gen-ops)
+ (stx-map
+ (syntax-parser
+ [(~∀ _ (~ext-stlc:→ ty_in ... _)) #'(ty_in ...)])
+ conc-op-tys)))
+ #'((generic-op ...) ...) #'((ty-concrete-op ...) ...) #'(TC ...))
+ ;; ) arity check
+ #:fail-unless (stx-length=? #'(τ_in ...) #'e_args)
+ (mk-app-err-msg stx #:expected #'(τ_in ...)
+ #:note "Wrong number of arguments.")
+ ;; ) compute argument types; re-use args expanded during solve
+ #:with ([e_arg2- τ_arg2] ...) (let ([n (stx-length #'(e_arg1- ...))])
+ (infers+erase
+ (stx-map add-expected-ty
+ (stx-drop #'e_args n) (stx-drop #'(τ_in ...) n))))
+ #:with (τ_arg1 ...) (stx-map typeof #'(e_arg1- ...))
+ #:with (τ_arg ...) #'(τ_arg1 ... τ_arg2 ...)
+ #:with (e_arg- ...) #'(e_arg1- ... e_arg2- ...)
+ ;; ) typecheck args
+ #:fail-unless (typechecks? #'(τ_arg ...) #'(τ_in ...))
+ (mk-app-err-msg stx
+ #:given #'(τ_arg ...)
+ #:expected
+ (stx-map
+ (lambda (tyin)
+ (define old-orig (get-orig tyin))
+ (define new-orig
+ (and old-orig
+ (substs
+ (stx-map get-orig (lookup-Xs/keep-unsolved #'Xs #'cs)) #'Xs old-orig
+ (lambda (x y)
+ (equal? (syntax->datum x) (syntax->datum y))))))
+ (syntax-property tyin 'orig (list new-orig)))
+ #'(τ_in ...)))
+ #:with τ_out* (if (stx-null? #'(unsolved-X ...))
+ #'τ_out
+ (syntax-parse #'τ_out
+ [(~?∀ (Y ...) τ_out)
+ (unless (→? #'τ_out)
+ (raise-app-poly-infer-error stx #'(τ_in ...) #'(τ_arg ...) #'e_fn))
+ #'(∀ (unsolved-X ... Y ...) τ_out)]))
+ (⊢ ((#%app- e_fn- op ...) e_arg- ...) : τ_out*)])])])]
+ [(_ e_fn . e_args) ; err case; e_fn is not a function
+ #:with [e_fn- τ_fn] (infer+erase #'e_fn)
+ (type-error #:src stx
+ #:msg (format "Expected expression ~a to have → type, got: ~a"
+ (syntax->datum #'e_fn) (type->str #'τ_fn)))])
+
+
+;; cond and other conditionals
+(define-typed-syntax cond
+ [(_ [(~or (~and (~datum else) (~parse test #'(ext-stlc:#%datum . #t)))
+ test)
+ b ... body] ...+)
+ #:with (test- ...) (⇑s (test ...) as Bool)
+ #:with ty-expected (get-expected-type stx)
+ #:with ([body- ty_body] ...) (infers+erase #'((add-expected body ty-expected) ...))
+ #:with (([b- ty_b] ...) ...) (stx-map infers+erase #'((b ...) ...))
+ #:with τ_out (stx-foldr (current-join) (stx-car #'(ty_body ...)) (stx-cdr #'(ty_body ...)))
+ (⊢ (cond- [test- b- ... body-] ...) : τ_out)])
+(define-typed-syntax when
+ [(_ test body ...)
+; #:with test- (⇑ test as Bool)
+ #:with [test- _] (infer+erase #'test)
+ #:with [(body- _) ...] (infers+erase #'(body ...))
+ (⊢ (when- test- body- ...) : Unit)])
+(define-typed-syntax unless
+ [(_ test body ...)
+; #:with test- (⇑ test as Bool)
+ #:with [test- _] (infer+erase #'test)
+ #:with [(body- _) ...] (infers+erase #'(body ...))
+ (⊢ (unless- test- body- ...) : Unit)])
+
+;; sync channels and threads
+(define-type-constructor Channel)
+
+(define-typed-syntax make-channel
+ [(_ (~and tys {ty}))
+ #:when (brace? #'tys)
+ (⊢ (make-channel-) : (Channel ty))])
+(define-typed-syntax channel-get
+ [(_ c)
+ #:with (c- (ty)) (⇑ c as Channel)
+ (⊢ (channel-get- c-) : ty)])
+(define-typed-syntax channel-put
+ [(_ c v)
+ #:with (c- (ty)) (⇑ c as Channel)
+ #:with [v- ty_v] (infer+erase #'v)
+ #:fail-unless (typechecks? #'ty_v #'ty)
+ (format "Cannot send ~a value on ~a channel."
+ (type->str #'ty_v) (type->str #'ty))
+ (⊢ (channel-put- c- v-) : Unit)])
+
+(define-base-type Thread)
+
+;; threads
+(define-typed-syntax thread
+ [(_ th)
+ #:with (th- (~∀ () (~ext-stlc:→ τ_out))) (infer+erase #'th)
+ (⊢ (thread- th-) : Thread)])
+
+(define-primop random : (→ Int Int))
+(define-primop integer->char : (→ Int Char))
+(define-primop string->list : (→ String (List Char)))
+(define-primop string->number : (→ String Int))
+;(define-primop number->string : (→ Int String))
+(define-typed-syntax num->str #:export-as number->string
+ [f:id (assign-type #'number->string #'(→ Int String))]
+ [(_ n)
+ #'(num->str n (ext-stlc:#%datum . 10))]
+ [(_ n rad)
+ #:with args- (⇑s (n rad) as Int)
+ (⊢ (number->string- . args-) : String)])
+(define-primop string : (→ Char String))
+(define-primop sleep : (→ Int Unit))
+(define-primop string=? : (→ String String Bool))
+(define-primop string<? : (→ String String Bool))
+(define-primop string<=? : (→ String String Bool))
+(define-primop string>? : (→ String String Bool))
+(define-primop string>=? : (→ String String Bool))
+(define-primop char=? : (→ Char Char Bool))
+(define-primop char<? : (→ Char Char Bool))
+(define-primop char<=? : (→ Char Char Bool))
+(define-primop char>? : (→ Char Char Bool))
+(define-primop char>=? : (→ Char Char Bool))
+
+(define-typed-syntax string-append
+ [(_ . strs)
+ #:with strs- (⇑s strs as String)
+ (⊢ (string-append- . strs-) : String)])
+
+;; vectors
+(define-type-constructor Vector)
+
+(define-typed-syntax vector
+ [(_ (~and tys {ty}))
+ #:when (brace? #'tys)
+ (⊢ (vector-) : (Vector ty))]
+ [(_ v ...)
+ #:with ([v- ty] ...) (infers+erase #'(v ...))
+ #:when (same-types? #'(ty ...))
+ #:with one-ty (stx-car #'(ty ...))
+ (⊢ (vector- v- ...) : (Vector one-ty))])
+(define-typed-syntax make-vector/tc #:export-as make-vector
+ [(_ n) #'(make-vector/tc n (ext-stlc:#%datum . 0))]
+ [(_ n e)
+ #:with n- (⇑ n as Int)
+ #:with [e- ty] (infer+erase #'e)
+ (⊢ (make-vector- n- e-) : (Vector ty))])
+(define-typed-syntax vector-length
+ [(_ e)
+ #:with [e- _] (⇑ e as Vector)
+ (⊢ (vector-length- e-) : Int)])
+(define-typed-syntax vector-ref
+ [(_ e n)
+ #:with n- (⇑ n as Int)
+ #:with [e- (ty)] (⇑ e as Vector)
+ (⊢ (vector-ref- e- n-) : ty)])
+(define-typed-syntax vector-set!
+ [(_ e n v)
+ #:with n- (⇑ n as Int)
+ #:with [e- (ty)] (⇑ e as Vector)
+ #:with [v- ty_v] (infer+erase #'v)
+ #:when (typecheck? #'ty_v #'ty)
+ (⊢ (vector-set!- e- n- v-) : Unit)])
+(define-typed-syntax vector-copy!
+ [(_ dest start src)
+ #:with start- (⇑ start as Int)
+ #:with [dest- (ty_dest)] (⇑ dest as Vector)
+ #:with [src- (ty_src)] (⇑ src as Vector)
+ #:when (typecheck? #'ty_dest #'ty_src)
+ (⊢ (vector-copy!- dest- start- src-) : Unit)])
+
+
+;; sequences and for loops
+
+(define-type-constructor Sequence)
+
+(define-typed-syntax in-range/tc #:export-as in-range
+ [(_ end)
+ #'(in-range/tc (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]
+ [(_ start end)
+ #'(in-range/tc start end (ext-stlc:#%datum . 1))]
+ [(_ start end step)
+ #:with (e- ...) (⇑s (start end step) as Int)
+ (⊢ (in-range- e- ...) : (Sequence Int))])
+
+(define-typed-syntax in-naturals/tc #:export-as in-naturals
+ [(_) #'(in-naturals/tc (ext-stlc:#%datum . 0))]
+ [(_ start)
+ #:with start- (⇑ start as Int)
+ (⊢ (in-naturals- start-) : (Sequence Int))])
+
+
+(define-typed-syntax in-vector
+ [(_ e)
+ #:with [e- (ty)] (⇑ e as Vector)
+ (⊢ (in-vector- e-) : (Sequence ty))])
+
+(define-typed-syntax in-list
+ [(_ e)
+ #:with [e- (ty)] (⇑ e as List)
+ (⊢ (in-list- e-) : (Sequence ty))])
+
+(define-typed-syntax in-lines
+ [(_ e)
+ #:with e- (⇑ e as String)
+ (⊢ (in-lines- (open-input-string- e-)) : (Sequence String))])
+
+(define-typed-syntax for
+ [(_ ([x:id e]...) b ... body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) (b- ... body-) (ty_b ... ty_body)]
+ (infers/ctx+erase #'([x : ty] ...) #'(b ... body))
+ (⊢ (for- ([x- e-] ...) b- ... body-) : Unit)])
+(define-typed-syntax for*
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for*- ([x- e-] ...) body-) : Unit)])
+
+(define-typed-syntax for/list
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for/list- ([x- e-] ...) body-) : (List ty_body))])
+(define-typed-syntax for/vector
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for/vector- ([x- e-] ...) body-) : (Vector ty_body))])
+(define-typed-syntax for*/vector
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for*/vector- ([x- e-] ...) body-) : (Vector ty_body))])
+(define-typed-syntax for*/list
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for*/list- ([x- e-] ...) body-) : (List ty_body))])
+(define-typed-syntax for/fold
+ [(_ ([acc init]) ([x:id e] ...) body)
+ #:with [init- ty_init] (infer+erase #`(pass-expected init #,stx))
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(acc- x- ...) body- ty_body]
+ (infer/ctx+erase #'([acc : ty_init][x : ty] ...) #'body)
+ #:fail-unless (typecheck? #'ty_body #'ty_init)
+ (type-error #:src stx
+ #:msg
+ "for/fold: Type of body and initial accumulator must be the same, given ~a and ~a"
+ #'ty_init #'ty_body)
+ (⊢ (for/fold- ([acc- init-]) ([x- e-] ...) body-) : ty_body)])
+
+(define-typed-syntax for/hash
+ [(_ ([x:id e]...) body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) body- (~× ty_k ty_v)]
+ (infer/ctx+erase #'([x : ty] ...) #'body)
+ (⊢ (for/hash- ([x- e-] ...) (let- ([t body-]) (values- (car- t) (cadr- t))))
+ : (Hash ty_k ty_v))])
+
+(define-typed-syntax for/sum
+ [(_ ([x:id e]...
+ (~optional (~seq #:when guard) #:defaults ([guard #'#t])))
+ body)
+ #:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
+ #:with [(x- ...) (guard- body-) (_ ty_body)]
+ (infers/ctx+erase #'([x : ty] ...) #'(guard body))
+ #:when (Int? #'ty_body)
+ (⊢ (for/sum- ([x- e-] ... #:when guard-) body-) : Int)])
+
+; printing and displaying
+(define-typed-syntax printf
+ [(_ str e ...)
+ #:with s- (⇑ str as String)
+ #:with ([e- ty] ...) (infers+erase #'(e ...))
+ (⊢ (printf- s- e- ...) : Unit)])
+(define-typed-syntax format
+ [(_ str e ...)
+ #:with s- (⇑ str as String)
+ #:with ([e- ty] ...) (infers+erase #'(e ...))
+ (⊢ (format- s- e- ...) : String)])
+(define-typed-syntax display
+ [(_ e)
+ #:with [e- _] (infer+erase #'e)
+ (⊢ (display- e-) : Unit)])
+(define-typed-syntax displayln
+ [(_ e)
+ #:with [e- _] (infer+erase #'e)
+ (⊢ (displayln- e-) : Unit)])
+(define-primop newline : (→ Unit))
+
+(define-typed-syntax list->vector
+ [(_ e)
+ #:with [e- (ty)] (⇑ e as List)
+ (⊢ (list->vector- e-) : (Vector ty))])
+
+(define-typed-syntax let
+ [(_ name:id (~datum :) ty:type ~! ([x:id e] ...) b ... body)
+ #:with ([e- ty_e] ...) (infers+erase #'(e ...))
+ #:with [(name- . xs-) (body- ...) (_ ... ty_body)]
+ (infers/ctx+erase #'([name : (→ ty_e ... ty.norm)][x : ty_e] ...)
+ #'(b ... body))
+ #:fail-unless (typecheck? #'ty_body #'ty.norm)
+ (format "type of let body ~a does not match expected typed ~a"
+ (type->str #'ty_body) (type->str #'ty))
+ (⊢ (letrec- ([name- (λ- xs- body- ...)])
+ (name- e- ...))
+ : ty_body)]
+ [(_ ([x:id e] ...) body ...)
+ #'(ext-stlc:let ([x e] ...) (begin/tc body ...))])
+(define-typed-syntax let*
+ [(_ ([x:id e] ...) body ...)
+ #'(ext-stlc:let* ([x e] ...) (begin/tc body ...))])
+
+(define-typed-syntax begin/tc #:export-as begin
+ [(_ body ... b)
+ #:with expected (get-expected-type stx)
+ #:with b_ann #'(add-expected b expected)
+ #'(ext-stlc:begin body ... b_ann)])
+
+;; hash
+(define-type-constructor Hash #:arity = 2)
+
+(define-typed-syntax in-hash
+ [(_ e)
+ #:with [e- (ty_k ty_v)] (⇑ e as Hash)
+ (⊢ (map- (λ- (k+v) (list- (car- k+v) (cdr- k+v))) (hash->list- e-))
+; (⊢ (hash->list e-)
+ : (Sequence (stlc+rec-iso:× ty_k ty_v)))])
+
+; mutable hashes
+(define-typed-syntax hash
+ [(_ (~and tys {ty_key ty_val}))
+ #:when (brace? #'tys)
+ (⊢ (make-hash-) : (Hash ty_key ty_val))]
+ [(_ (~seq k v) ...)
+ #:with ([k- ty_k] ...) (infers+erase #'(k ...))
+ #:with ([v- ty_v] ...) (infers+erase #'(v ...))
+ #:when (same-types? #'(ty_k ...))
+ #:when (same-types? #'(ty_v ...))
+ #:with ty_key (stx-car #'(ty_k ...))
+ #:with ty_val (stx-car #'(ty_v ...))
+ (⊢ (make-hash- (list- (cons- k- v-) ...)) : (Hash ty_key ty_val))])
+(define-typed-syntax hash-set!
+ [(_ h k v)
+ #:with [h- (ty_key ty_val)] (⇑ h as Hash)
+ #:with [k- ty_k] (infer+erase #'k)
+ #:with [v- ty_v] (infer+erase #'v)
+ #:when (typecheck? #'ty_k #'ty_key)
+ #:when (typecheck? #'ty_v #'ty_val)
+ (⊢ (hash-set!- h- k- v-) : Unit)])
+(define-typed-syntax hash-ref/tc #:export-as hash-ref
+ [(_ h k) #'(hash-ref/tc h k (ext-stlc:#%datum . #f))]
+ [(_ h k fail)
+ #:with [h- (ty_key ty_val)] (⇑ h as Hash)
+ #:with [k- ty_k] (infer+erase #'k)
+ #:when (typecheck? #'ty_k #'ty_key)
+ #:with (fail- _) (infer+erase #'fail) ; default val can be any
+ (⊢ (hash-ref- h- k- fail-) : ty_val)])
+(define-typed-syntax hash-has-key?
+ [(_ h k)
+ #:with [h- (ty_key _)] (⇑ h as Hash)
+ #:with [k- ty_k] (infer+erase #'k)
+ #:when (typecheck? #'ty_k #'ty_key)
+ (⊢ (hash-has-key?- h- k-) : Bool)])
+
+(define-typed-syntax hash-count
+ [(_ h)
+ #:with [h- _] (⇑ h as Hash)
+ (⊢ (hash-count- h-) : Int)])
+
+(define-base-type String-Port)
+(define-base-type Input-Port)
+(define-primop open-output-string : (→ String-Port))
+(define-primop get-output-string : (→ String-Port String))
+(define-primop string-upcase : (→ String String))
+
+(define-typed-syntax write-string/tc #:export-as write-string
+ [(_ str out)
+ #'(write-string/tc str out (ext-stlc:#%datum . 0) (string-length/tc str))]
+ [(_ str out start end)
+ #:with str- (⇑ str as String)
+ #:with out- (⇑ out as String-Port)
+ #:with start- (⇑ start as Int)
+ #:with end- (⇑ end as Int)
+ (⊢ (write-string- str- out- start- end-) : Unit)])
+
+(define-typed-syntax string-length/tc #:export-as string-length
+ [(_ str)
+ #:with str- (⇑ str as String)
+ (⊢ (string-length- str-) : Int)])
+(define-primop make-string : (→ Int String))
+(define-primop string-set! : (→ String Int Char Unit))
+(define-primop string-ref : (→ String Int Char))
+(define-typed-syntax string-copy!/tc #:export-as string-copy!
+ [(_ dest dest-start src)
+ #'(string-copy!/tc
+ dest dest-start src (ext-stlc:#%datum . 0) (string-length/tc src))]
+ [(_ dest dest-start src src-start src-end)
+ #:with dest- (⇑ dest as String)
+ #:with src- (⇑ src as String)
+ #:with dest-start- (⇑ dest-start as Int)
+ #:with src-start- (⇑ src-start as Int)
+ #:with src-end- (⇑ src-end as Int)
+ (⊢ (string-copy!- dest- dest-start- src- src-start- src-end-) : Unit)])
+
+(define-primop fl+ : (→ Float Float Float))
+(define-primop fl- : (→ Float Float Float))
+(define-primop fl* : (→ Float Float Float))
+(define-primop fl/ : (→ Float Float Float))
+(define-primop fl= : (→ Float Float Bool))
+(define-primop flsqrt : (→ Float Float))
+(define-primop flceiling : (→ Float Float))
+(define-primop inexact->exact : (→ Float Int))
+(define-primop exact->inexact : (→ Int Float))
+(define-primop char->integer : (→ Char Int))
+(define-primop real->decimal-string : (→ Float Int String))
+(define-primop fx->fl : (→ Int Float))
+(define-typed-syntax quotient+remainder
+ [(_ x y)
+ #:with x- (⇑ x as Int)
+ #:with y- (⇑ y as Int)
+ (⊢ (call-with-values- (λ- () (quotient/remainder- x- y-)) list-)
+ : (stlc+rec-iso:× Int Int))])
+(define-primop quotient : (→ Int Int Int))
+
+(define-typed-syntax set!
+ [(_ x:id e)
+ #:with [x- ty_x] (infer+erase #'x)
+ #:with [e- ty_e] (infer+erase #'e)
+ #:when (typecheck? #'ty_e #'ty_x)
+ (⊢ (set!- x e-) : Unit)])
+
+(define-typed-syntax provide-type [(_ ty ...) #'(provide- ty ...)])
+
+(define-typed-syntax provide
+ [(_ x:id ...)
+ #:with ([x- ty_x] ...) (infers+erase #'(x ...))
+ ; TODO: use hash-code to generate this tmp
+ #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
+ #'(begin-
+ (provide- x ...)
+ (stlc+rec-iso:define-type-alias x-ty ty_x) ...
+ (provide- x-ty ...))])
+(define-typed-syntax require-typed
+ [(_ x:id ... #:from mod)
+ #:with (x-ty ...) (stx-map (lambda (y) (format-id y "~a-ty" y)) #'(x ...))
+ #:with (y ...) (generate-temporaries #'(x ...))
+ #'(begin-
+ (require- (rename-in- (only-in- mod x ... x-ty ...) [x y] ...))
+ (define-syntax- x (make-rename-transformer (assign-type #'y #'x-ty))) ...)])
+
+(define-base-type Regexp)
+(define-primop regexp-match : (→ Regexp String (List String)))
+(define-primop regexp : (→ String Regexp))
+
+(define-typed-syntax equal?
+ [(_ e1 e2)
+ #:with [e1- ty1] (infer+erase #'e1)
+ #:with [e2- ty2] (infer+erase #'(add-expected e2 ty1))
+ #:fail-unless (typecheck? #'ty1 #'ty2) "arguments to equal? have different types"
+ (⊢ (equal?- e1- e2-) : Bool)])
+
+(define-syntax (inst stx)
+ (syntax-parse stx
+ [(_ e ty ...)
+ #:with [ee tyty] (infer+erase #'e)
+ #:with [e- ty_e] (infer+erase #'(sysf:inst e ty ...))
+ #:with ty_out (cond
+ [(→? #'ty_e) #'(∀ () ty_e)]
+ [(=>? #'ty_e) #'(∀ () ty_e)]
+ [else #'ty_e])
+ (⊢ e- : ty_out)]))
+
+(define-typed-syntax read
+ [(_)
+ (⊢ (let- ([x (read-)])
+ (cond- [(eof-object?- x) ""]
+ [(number?- x) (number->string- x)]
+ [(symbol?- x) (symbol->string- x)])) : String)])
+
+(begin-for-syntax
+ ;; - this function should be wrapped with err handlers,
+ ;; for when an op with the specified generic op and input types does not exist,
+ ;; otherwise, will get "unbound id" err with internal mangled id
+ ;; - gen-op must be identifier, eg should already have proper context
+ ;; and mangled-op is selected based on input types,
+ ;; ie, dispatch to different concrete fns based on input tpyes
+ ;; TODO: currently using input types only, but sometimes may need output type
+ ;; eg, Read typeclass, this is currently unsupported
+ ;; - need to use expected-type?
+ (define (lookup-op gen-op tys)
+ (define (transfer-gen-op-ctx o) (format-id gen-op "~a" o))
+ (define (transfer-gen-op-ctxs os) (stx-map transfer-gen-op-ctx os))
+ (syntax-parse tys
+ ;; TODO: for now, only handle uniform tys, ie tys must be all
+ ;; tycons or all base types or all tyvars
+ ;; tycon --------------------------------------------------
+ ;; - recur on ty-args
+ [(((~literal #%plain-app) tycon
+ ((~literal #%plain-lambda) _ _ ty-arg ...)) ...)
+ ;; 1) look up concrete op corresponding to generic op and input tys
+ #:with mangled (mangle gen-op #'(tycon ...))
+ #:with [conc-op ty-conc-op] (infer+erase #'mangled)
+ ;; compute sub-ops based on TC constraints (will include gen-op --- for smaller type)
+ #:with (~∀ Xs (~=> TC ... (~ext-stlc:→ . ty-args))) #'ty-conc-op
+ #:with (~TCs ([op _] ...) ...) #'(TC ...) ; order matters, must match order of arg types
+ #:with ((sub-op ...) ...) (stx-map transfer-gen-op-ctxs #'((op ...) ...))
+ ;; drop the TCs in result type, the proper subops are already applied
+ #:with ty-conc-op-noTC #'(∀ Xs (ext-stlc:→ . ty-args))
+ ;; recursively call lookup-op for each subop and input ty-args
+ (⊢ (conc-op
+ #,@(apply stx-appendmap (lambda (ops . tys) (stx-map (lambda (o) (lookup-op o tys)) ops))
+ #'((sub-op ...) ...)
+ (syntax->list #'((ty-arg ...) ...))))
+ : ty-conc-op-noTC)]
+ ;; base type --------------------------------------------------
+ [(((~literal #%plain-app) tag) ...) (expand/df (mangle gen-op #'(tag ...)))]
+ ;; tyvars --------------------------------------------------
+ [_ (expand/df (mangle gen-op tys))]))
+ (define (get-fn-ty-in-tags ty-fn)
+ (syntax-parse ty-fn
+ [(~∀ _ (~ext-stlc:→ ty_in ... _))
+ (get-type-tags #'(ty_in ...))]))
+ (define (TC-exists? TC #:ctx [ctx TC]) ; throws exn if fail
+ (syntax-parse TC
+ [(~TC-base [gen-op ty-op] . _) ; only need 1st op
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (lambda (e)
+ (type-error #:src ctx
+ #:msg "No instance defined for ~a" TC))])
+ (expand/df
+ (mangle (format-id ctx "~a" #'gen-op)
+ (get-fn-ty-in-tags #'ty-op))))]))
+ (define (TCs-exist? TCs #:ctx [ctx TCs])
+ (stx-map (lambda (tc) (TC-exists? tc #:ctx ctx)) TCs)))
+
+;; adhoc polymorphism
+;; TODO: make this a formal type?
+;; - or at least define a pattern expander - DONE 2016-05-01
+;; A TC is a #'(=> subclassTC ... ([generic-op gen-op-ty] ...))
+(define-syntax (define-typeclass stx)
+ (syntax-parse stx
+ [(~or (_ TC ... (~datum =>) (Name X ...) [op (~datum :) ty] ...)
+ (~and (_ (Name X ...) [op (~datum :) ty] ...) ; no subclass
+ (~parse (TC ...) #'())))
+ #'(begin-
+ (define-syntax- (op stx)
+ (syntax-parse stx
+ [(o . es)
+ #:with ([e- ty_e] (... ...)) (infers+erase #'es)
+ #:with out-op
+ (with-handlers
+ ([exn:fail:syntax:unbound?
+ (lambda (e)
+ (type-error #:src #'o
+ #:msg (format
+ "~a operation undefined for input types: ~a"
+ (syntax->datum #'o)
+ (types->str #'(ty_e (... ...))))))])
+ (lookup-op #'o #'(ty_e (... ...))))
+ #:with app (datum->syntax #'o '#%app)
+ (datum->syntax stx (cons #'app (cons #'out-op #'(e- (... ...)))))])) ...
+ (define-syntax- (Name stx)
+ (syntax-parse stx
+ [(_ X ...)
+ (add-orig
+ #`(=> TC ... #,(mk-type #'(('op ty) ...)))
+ #'(Name X ...))])))]))
+
+(define-syntax (define-instance stx)
+ (syntax-parse stx
+ ;; base type, possibly with subclasses ------------------------------------
+ [(_ (Name ty ...) [generic-op concrete-op] ...)
+ #:with (~=> TC ... (~TC [generic-op-expected ty-concrete-op-expected] ...))
+ (expand/df #'(Name ty ...))
+ #:when (TCs-exist? #'(TC ...) #:ctx stx)
+ #:fail-unless (set=? (syntax->datum #'(generic-op ...))
+ (syntax->datum #'(generic-op-expected ...)))
+ (type-error #:src stx
+ #:msg (format "Type class instance ~a incomplete, missing: ~a"
+ (syntax->datum #'(Name ty ...))
+ (string-join
+ (map symbol->string
+ (set-subtract (syntax->datum #'(generic-op-expected ...))
+ (syntax->datum #'(generic-op ...))))
+ ", ")))
+ ;; sort, using order from define-typeclass
+ #:with ([generic-op-sorted concrete-op-sorted] ...)
+ (stx-map
+ (lambda (expected-op)
+ (stx-findf
+ (lambda (gen+conc)
+ (equal? (syntax->datum (stx-car gen+conc))
+ (syntax->datum expected-op)))
+ #'([generic-op concrete-op] ...)))
+ #'(generic-op-expected ...))
+ ;; typecheck type of given concrete-op with expected type from define-typeclass
+ #:with ([concrete-op+ ty-concrete-op] ...) (infers+erase #'(concrete-op-sorted ...))
+ #:fail-unless (typechecks? #'(ty-concrete-op ...) #'(ty-concrete-op-expected ...))
+ (mk-app-err-msg (syntax/loc stx (#%app (Name ty ...) concrete-op ...))
+ #:expected #'(ty-concrete-op-expected ...)
+ #:given #'(ty-concrete-op ...)
+ #:action "defining typeclass instance"
+ #:name (format "~a" (syntax->datum #'(Name ty ...))))
+ ;; generate mangled name from tags in input types
+ #:with (ty_in-tags ...)
+ (stx-map
+ (syntax-parser
+ [(~∀ _ (~ext-stlc:→ ty_in ... _))
+ (get-type-tags #'(ty_in ...))])
+ #'(ty-concrete-op-expected ...))
+ ;; use input types
+ #:with (mangled-op ...) (stx-map mangle #'(generic-op ...) #'(ty_in-tags ...))
+ #'(begin-
+ (define-syntax- (mangled-op stx)
+ (syntax-parse stx [_:id (assign-type #'concrete-op+ #'ty-concrete-op-expected)]))
+ ...)]
+ ;; tycon, possibly with subclasses -----------------------------------------
+ [(_ TC ... (~datum =>) (Name ty ...) [generic-op concrete-op] ...)
+ #:with (X ...) (compute-tyvars #'(ty ...))
+ ;; ok to drop TCsub ...? I think yes
+ ;; - the same TCsubs will be part of TC+,
+ ;; so proper op will be looked up, depending on input args,
+ ;; using inherited ops in TC+
+ ;; This is assuming Name and TC ... are the same typeclass
+ ;; Won't work for, eg (TC1 (List X)) that depends on some other (TC2 X)
+ #:with (Xs+
+ (TC+ ...
+ (~=> TCsub ...
+ (~TC [generic-op-expected ty-concrete-op-expected] ...)))
+ _)
+ (infers/tyctx+erase #'([X : #%type] ...) #'(TC ... (Name ty ...)))
+ #:when (TCs-exist? #'(TCsub ...) #:ctx stx)
+ ;; simulate as if the declared concrete-op* has TC ... predicates
+ ;; TODO: fix this manual deconstruction and assembly
+ #:with ((app fa (lam _ ei ty_fn)) ...) #'(ty-concrete-op-expected ...)
+ #:with (ty-concrete-op-expected-withTC ...)
+ (stx-map (current-type-eval) #'((app fa (lam Xs+ ei (=> TC+ ... ty_fn))) ...))
+ #:fail-unless (set=? (syntax->datum #'(generic-op ...))
+ (syntax->datum #'(generic-op-expected ...)))
+ (type-error #:src stx
+ #:msg (format "Type class instance ~a incomplete, missing: ~a"
+ (syntax->datum #'(Name ty ...))
+ (string-join
+ (map symbol->string
+ (set-subtract (syntax->datum #'(generic-op-expected ...))
+ (syntax->datum #'(generic-op ...))))
+ ", ")))
+ ;; - sort, using order from define-typeclass
+ ;; - insert TC ... if lambda
+ #:with ([generic-op-sorted concrete-op-sorted] ...)
+ (stx-map
+ (lambda (expected-op)
+ (syntax-parse
+ (stx-findf
+ (lambda (gen+conc)
+ (equal? (syntax->datum (stx-car gen+conc))
+ (syntax->datum expected-op)))
+ #'([generic-op concrete-op] ...))
+ [(g c)
+ (syntax-parse #'c
+ ;; add TCs to (unexpanded) lambda
+ [((~and lam (~literal liftedλ)) (args ...) . body)
+ #'(g (lam (args ... #:where TC ...) . body))]
+ [_ #'(g c)])]))
+ #'(generic-op-expected ...))
+ ;; ;; for now, dont expand (and typecheck) concrete-op
+ ;; #:with ([concrete-op+ ty-concrete-op] ...) (infers+erase #'(concrete-op ...))
+ ;; #:when (typechecks? #'(ty-concrete-op ...) #'(ty-concrete-op-expected ...))
+ ;; TODO: right now, dont recur to get nested tags
+ ;; but may need to do so, ie if an instance needs to define more than one concrete op,
+ ;; eg (define-instance (Eq (List Int)) ...)
+ #:with (ty_in-tags ...)
+ (stx-map
+ (syntax-parser
+ [(~∀ _ (~ext-stlc:→ ty_in ... _))
+ (get-type-tags #'(ty_in ...))]
+ #;[(~∀ _ (~=> _ ... (~ext-stlc:→ ty_in ... _)))
+ (get-type-tags #'(ty_in ...))])
+ #'(ty-concrete-op-expected ...))
+ #:with (mangled-op ...) (stx-map mangle #'(generic-op ...) #'(ty_in-tags ...))
+ ;; need a name for concrete-op because concrete-op and generic-op may be
+ ;; mutually recursive, eg (Eq (List X))
+ #:with (f ...) (generate-temporaries #'(concrete-op-sorted ...))
+ #'(begin-
+ (define- f concrete-op-sorted) ...
+ (define-syntax- (mangled-op stx)
+ (syntax-parse stx [_:id (assign-type #'f #'ty-concrete-op-expected-withTC)]))
+ ...)]))
diff --git a/turnstile/examples/tests/mlish/generic.mlish b/turnstile/examples/tests/mlish/generic.mlish
@@ -0,0 +1,461 @@
+#lang s-exp "../../mlish+adhoc.rkt"
+(require "../rackunit-typechecking.rkt")
+
+(define-typeclass (Eq X)
+ [== : (→ X X Bool)])
+
+(define-instance (Eq Int)
+ [== =])
+
+(define-instance (Eq Float)
+ [== fl=])
+
+(define (id-fn1 [x : X] #:where (Eq X) -> X) x)
+(typecheck-fail (id-fn1 #f) #:with-msg "\\(Eq Bool\\) instance undefined")
+(check-type (id-fn1 1) : Int -> 1)
+
+(check-type (== 1 2) : Bool -> (= 1 2))
+(check-type (== 1 2) : Bool -> #f)
+(check-type (== 2 2) : Bool -> (= 2 2))
+(check-type (== 2 2) : Bool -> #t)
+(typecheck-fail (== "1" "1")
+ #:with-msg "== operation undefined for input types: String, String")
+
+(define-instance (Eq String) ; test use of lambda on rhs
+ [== (λ ([x : String] [y : String])
+ (string=? x y))])
+
+(check-type (== "1" "2") : Bool -> (string=? "1" "2"))
+(check-type (== "1" "2") : Bool -> #f)
+(check-type (== "2" "2") : Bool -> (string=? "2" "2"))
+(check-type (== "2" "2") : Bool -> #t)
+
+(define-instance (Eq Char)
+ [== char=?])
+
+(check-type (λ ([x : X] #:where (Eq X))
+ (== x x))
+ : (=>/test (Eq X) (→ X Bool)))
+
+(check-type ((λ ([x : X] #:where (Eq X)) (== x x)) 1) : Bool -> #t)
+(check-type ((λ ([x : X] #:where (Eq X)) (== x x)) "1") : Bool -> #t)
+(typecheck-fail ((λ ([x : X] #:where (Eq X)) (== x x)) #f)
+ #:with-msg
+ "Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool")
+
+(define (member? [x : X] [lst : (List X)] #:where (Eq X) -> Bool)
+ (match lst with
+ [[] -> #f]
+ [y :: ys -> (or (== x y) (member? x ys))]))
+
+(check-type (member? 1 nil) : Bool -> #f)
+(check-type (member? 1 (list 2)) : Bool -> #f)
+(check-type (member? 1 (list 2 1)) : Bool -> #t)
+(typecheck-fail (member? "1" (list 1))) ; TODO: fix err msg
+(check-type (member? "1" nil) : Bool -> #f)
+(check-type (member? "1" (list "2")) : Bool -> #f)
+(check-type (member? "1" (list "2" "1")) : Bool -> #t)
+
+;; TODO?: fix name clash of generic op and concrete op
+(define-typeclass (Ord X)
+ [lt : (→ X X Bool)]
+ [lte : (→ X X Bool)]
+ [gt : (→ X X Bool)]
+ [gte : (→ X X Bool)])
+
+(define-instance (Ord Int)
+ [lt <] [lte <=] [gt >] [gte >=])
+
+;; missing typeclass constraint
+(typecheck-fail (λ ([x : X]) (== x x))
+ #:with-msg "== operation undefined for input types: X, X")
+(typecheck-fail (λ ([x : X]) (lte x x))
+ #:with-msg "lte operation undefined for input types: X, X")
+;; wrong typeclass constraint
+(typecheck-fail (λ ([x : Y] #:where (Ord Y)) (== x x))
+ #:with-msg "== operation undefined for input types: Y, Y")
+(typecheck-fail (λ ([x : Y] #:where (Eq Y)) (gt x x))
+ #:with-msg "gt operation undefined for input types: Y, Y")
+
+(check-type (λ ([x : Y] #:where (Ord Y)) (lte x x))
+ : (=>/test (Ord Y) (→ Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y)) (lt x x))
+ : (=>/test (Ord Y) (→ Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y)) (gte x x))
+ : (=>/test (Ord Y) (→ Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y)) (gt x x))
+ : (=>/test (Ord Y) (→ Y Bool)))
+
+(check-type (λ ([x : Y] [y : Y] #:where (Ord Y)) (lt x x))
+ : (=>/test (Ord Y) (→ Y Y Bool)))
+(check-type (λ ([x : Y] [y : Y] #:where (Ord Y)) (lt x y))
+ : (=>/test (Ord Y) (→ Y Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y) (Eq Y))
+ (lt x x))
+ : (=>/test (Ord Y) (Eq Y) (→ Y Bool)))
+(check-type (λ ([x : Y] #:where (Ord Y) (Eq Y))
+ (== x x))
+ : (=>/test (Ord Y) (Eq Y) (→ Y Bool)))
+
+(check-type (λ ([x : Y] #:where (Ord Y) (Eq Y))
+ (and (== x x) (lte x x)))
+ : (=>/test (Ord Y) (Eq Y) (→ Y Bool)))
+
+;; todo: not working; results in dup ids
+#;(check-type (λ ([x : X] [y : Y] #:where (Ord X) (Ord Y)) (< x y))
+ : (=>/test (Ord Y) (→ Y Y Bool)))
+
+(define (f [x : X] #:where (Eq X) -> Bool)
+ (== x x))
+(check-type (f 1) : Bool -> #t)
+(check-type (f "1") : Bool -> #t)
+(typecheck-fail (f #f)
+ #:with-msg
+ "Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool")
+
+(define-instance (Ord String)
+ [lt string<?] [lte string<=?] [gt string>?] [gte string>=?])
+(check-type (lt "1" "2") : Bool -> #t)
+(define (f2 [x : X] [y : X] #:where (Ord X) -> Bool)
+ (lte x y))
+(check-type (f2 1 2) : Bool -> #t)
+(check-type (f2 "1" "2") : Bool -> #t)
+(typecheck-fail (f2 1 "2"))
+
+(define-typeclass (Num X)
+ [add : (→ X X X)]
+ [sub : (→ X X X)]
+ [mul : (→ X X X)])
+
+(typecheck-fail
+ (define-instance (Num Int)
+ [add +] [sub -] [mul fl*])
+ #:with-msg (string-append "Type error defining typeclass instance \\(Num Int\\).*"
+ (expected "(→ Int Int Int), (→ Int Int Int), (→ Int Int Int)"
+ #:given "(→ Int Int Int), (→ Int Int Int), (→ Float Float Float)")))
+
+(define-instance (Num Int)
+ [add +] [sub -] [mul *])
+(define-instance (Num Float)
+ [add fl+] [sub fl-] [mul fl*])
+
+(define (square [x : X] #:where (Num X) -> X)
+ (mul x x))
+(check-type (square 5) : Int -> 25)
+(check-type (square 2.5) : Float -> 6.25)
+;; "propagation" of typeclass constraints to other constrained fns
+;; (memsq tests the same thing?)
+(define (square2 [x : X] #:where (Num X) -> X)
+ (square x))
+(check-type (square2 5) : Int -> 25)
+(check-type (square2 2.5) : Float -> 6.25)
+(define (squares [xyz : (× X Y Z)] #:where (Num X) (Num Y) (Num Z)-> (× X Y Z))
+ (match2 xyz with
+ [(x,y,z) -> (tup (square x) (square y) (square z))]))
+(check-type (squares (tup 5 5 5)) : (× Int Int Int) -> (tup 25 25 25))
+(check-type (squares (tup 2.5 5 5)) : (× Float Int Int) -> (tup 6.25 25 25))
+(check-type (squares (tup 5 2.5 5)) : (× Int Float Int) -> (tup 25 6.25 25))
+(check-type (squares (tup 5 5 2.5)) : (× Int Int Float) -> (tup 25 25 6.25))
+(check-type (squares (tup 2.5 2.5 2.5)) : (× Float Float Float) -> (tup 6.25 6.25 6.25))
+(typecheck-fail (squares (tup 5 5 #f)) #:with-msg "\\(Num Bool\\) instance undefined")
+(typecheck-fail (squares (tup 5 #f 5)) #:with-msg "\\(Num Bool\\) instance undefined")
+(typecheck-fail (squares (tup #f 5 5)) #:with-msg "\\(Num Bool\\) instance undefined")
+
+;; --------------------------------------------------
+
+(define-type (TypeA X) (A [x : X] [y : X]))
+
+;; constraint of nested tyvar
+(define (test-a1 [a : (TypeA X)] #:where (Eq X) -> Bool)
+ (== (A-x a) (A-y a)))
+(check-type (test-a1 (A 1 2)) : Bool -> #f)
+(check-type (test-a1 (A "1" "2")) : Bool -> #f)
+(typecheck-fail (test-a1 (A #t #f))
+ #:with-msg
+"Eq Bool.*instance undefined.*Cannot instantiate function with constraints.*Eq X.*with.*X : Bool")
+
+(define (test-a2 [a : (TypeA X)] [fa : (→ (TypeA X) X)] #:where (Eq X) -> Bool)
+ (== (fa a) (fa a)))
+
+(check-type (test-a2 (A 1 2) (inst A-x Int)) : Bool -> #t)
+(check-type (test-a2 (A "1" "2") (inst A-x String)) : Bool -> #t)
+
+(define-type (Heap X)
+ Emp
+ (H X))
+
+(define (hf [h : (Heap X)] #:where (Ord X) -> Bool)
+ (match h with
+ [Emp -> #f]
+ [H x -> (lte x x)]))
+
+(check-type (hf (H 1)) : Bool -> #t)
+(typecheck-fail (hf (H #f))
+ #:with-msg
+ "Ord Bool.*instance undefined.*Cannot instantiate function with constraints.*Ord X.*with.*X : Bool")
+
+;; type classes for non-base types
+(define-instance (Eq X) => (Eq (List X))
+ [== (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> #t]
+ [((x :: xs),(y :: ys)) -> (and (== x y) (== xs ys))]
+ [_ -> #f]))])
+
+;; nil and nil
+(check-type (== (nil {Int}) (nil {Int})) : Bool -> #t)
+;; TODO: better err msg?
+;; as of 2016-04-04: "== operation undefined for input types: Int, Bool"
+;; should somehow indicate that the two values are not equal because types differ?
+(typecheck-fail (== (nil {Int}) (nil {Bool})))
+;; nil and non-nil
+(check-type (== (nil {Int}) (list 1)) : Bool -> #f)
+(check-type (== (nil {Int}) (cons 1 nil)) : Bool -> #f)
+(check-type (== (nil {Int}) (cons 1 (cons 2 nil))) : Bool -> #f)
+;; non-nil and nil
+(check-type (== (list 1) (nil {Int})) : Bool -> #f)
+(check-type (== (cons 1 nil) (nil {Int})) : Bool -> #f)
+(check-type (== (cons 1 (cons 2 nil)) (nil {Int})) : Bool -> #f)
+;; non-nil and non-nil
+(check-type (== (list 1) (list 1)) : Bool -> #t)
+(check-type (== (cons 1 nil) (list 1)) : Bool -> #t)
+(check-type (== (list 1) (cons 1 nil)) : Bool -> #t)
+(check-type (== (list 1) (list 1 2)) : Bool -> #f)
+(check-type (== (list 1 2) (list 1)) : Bool -> #f)
+(check-type (== (list 1 2) (list 1 2)) : Bool -> #t)
+(check-type (== (list 1 2) (list 1 3)) : Bool -> #f)
+(check-type (== (list 1 3) (list 1 2)) : Bool -> #f)
+
+(define (list-eq1 [l1 : (List X)] [l2 : (List X)] #:where (Eq X) -> Bool)
+ (== l1 l2))
+
+(check-type (list-eq1 (nil {Int}) (nil {Int})) : Bool -> #t)
+(check-type (list-eq1 (nil {Int}) (list 1)) : Bool -> #f)
+(check-type (list-eq1 (list 1) (nil {Int})) : Bool -> #f)
+(check-type (list-eq1 (list 1) (list 1)) : Bool -> #t)
+(check-type (list-eq1 (list 1) (list 2)) : Bool -> #f)
+(check-type (list-eq1 (list 1) (list 1 2)) : Bool -> #f)
+
+(check-type (member? (list 1) (list (list 1))) : Bool -> #t)
+(check-type (member? (list 1) (list (list 2))) : Bool -> #f)
+(check-type (member? (list 1) (list (list 2) (list 1))) : Bool -> #t)
+
+(define (id-fn2 [xs : (List X)] #:where (Eq X) -> (List X)) xs)
+(typecheck-fail (id-fn2 (list #f)) #:with-msg "\\(Eq Bool\\) instance undefined")
+(check-type (id-fn2 (list 1)) : (List Int) -> (list 1))
+
+;; TODO: #:where TC, where TC has a tycon, like #:where (List X)
+;; still doesnt work I dont think
+#;(define (list-eq2 [l1 : (List X)] [l2 : (List X)] #:where (List X) -> Bool)
+ (== l1 l2))
+
+;; TODO: implement subclasses
+;; 2016-05-25: Done. see memsq2
+(define (memsq? [x : X] [xs : (List X)] #:where (Eq X) (Num X) -> Bool)
+ (member? (square x) xs))
+(check-type (memsq? 1 (list 1)) : Bool -> #t)
+(check-type (memsq? 2 (list 2)) : Bool -> #f)
+(check-type (memsq? 2 (list 3 4)) : Bool -> #t)
+(typecheck-fail (memsq? (list 1) (list (list 1)))
+ #:with-msg "\\(Num \\(List Int\\)\\) instance undefined")
+
+
+(define (andmap [p? : (→ X Bool)] [lst : (List X)] -> Bool)
+ (match lst with
+ [[] -> #t]
+ [x :: xs -> (and (p? x) (andmap p? xs))]))
+
+;; Set
+;; type classes for non-base types: user-defined
+(define-type (Set X) (MkSet (List X)))
+(define-instance (Eq X) => (Eq (Set X))
+ [== (λ ([s1 : (Set X)] [s2 : (Set X)])
+ (match2 (tup s1 s2) with
+ [((MkSet xs),(MkSet ys)) -> (and (andmap (λ ([y : X]) (member? y xs)) ys)
+ (andmap (λ ([x : X]) (member? x ys)) xs))]))])
+(check-type (== (MkSet (list 1)) (MkSet (list 1))) : Bool -> #t)
+(check-type (== (MkSet (list 1)) (MkSet (list 2))) : Bool -> #f)
+(check-type (== (MkSet (list 1 2)) (MkSet (list 1 2))) : Bool -> #t)
+(check-type (== (MkSet (list 1 2)) (MkSet (list 2 1))) : Bool -> #t)
+(check-type (== (MkSet (list 1 2)) (MkSet (list 1 2 3))) : Bool -> #f)
+(check-type (== (MkSet (list 3 1 2)) (MkSet (list 1 2 3))) : Bool -> #t)
+
+(check-type (member? (MkSet (list 1 2)) (list (MkSet (list 1 2)))) : Bool -> #t)
+(check-type (member? (MkSet (list 1 2)) (list (MkSet (list 1)) (MkSet (list 2 1))))
+ : Bool -> #t)
+(check-type (member? (MkSet (list "1" "2")) (list (MkSet (list "1")) (MkSet (list "2" "1"))))
+ : Bool -> #t)
+
+;; type classes for non-base types: multiple constraints
+(define-instance (Eq X) (Eq Y) => (Eq (× X Y))
+ [== (λ ([p1 : (× X Y)] [p2 : (× X Y)])
+ (match2 (tup p1 p2) with
+ [((u,v),(x,y)) -> (and (== u x) (== v y))]))])
+
+(check-type (== (tup 1 2) (tup 3 4)) : Bool -> #f)
+(check-type (== (tup 1 2) (tup 1 2)) : Bool -> #t)
+(check-type (== (tup (list 1) (list 2)) (tup (list 1) (list 2))) : Bool -> #t)
+(check-type (== (tup (list 1) (list 1 2)) (tup (list 1) (list 2 1))) : Bool -> #f)
+(check-type (== (tup (list #\a) (list #\b)) (tup (list #\a) (list #\b)))
+ : Bool -> #t)
+(check-type (== (tup (list #\a) (list #\a #\b)) (tup (list #\a) (list #\b #\a)))
+ : Bool -> #f)
+
+(check-type (== (tup (list #\a) (list 1)) (tup (list #\a) (list 1)))
+ : Bool -> #t)
+(check-type (== (tup (list #\a) (list 1 2)) (tup (list #\a) (list 2 1)))
+ : Bool -> #f)
+
+(check-type (member? (tup 1 2) (list (tup 3 4) (tup 5 6))) : Bool -> #f)
+(check-type (member? (tup 1 2) (list (tup 3 4) (tup 5 6) (tup 1 2)))
+ : Bool -> #t)
+(check-type (member? (tup 1 "2") (list (tup 3 "4") (tup 5 "6")))
+ : Bool -> #f)
+(check-type (member? (tup 1 "2") (list (tup 3 "4") (tup 5 "6") (tup 1 "2")))
+ : Bool -> #t)
+(check-type
+ (member?
+ (tup (list 1) "2")
+ (list (tup (list 3) "4") (tup (list 5) "6")))
+ : Bool -> #f)
+(check-type
+ (member?
+ (tup (list 1) "2")
+ (list (tup (list 3) "4") (tup (list 5) "6") (tup (list 1) "2")))
+ : Bool -> #t)
+
+(define-typeclass (Eq X) => (Num2 X)
+ [ad : (→ X X X)]
+ [sb : (→ X X X)]
+ [mu : (→ X X X)])
+
+(typecheck-fail
+ (define-instance (Num2 Bool)
+ [ad +] [sb -] [mu *])
+ #:with-msg "No instance defined for \\(Eq Bool\\)")
+
+(define-instance (Num2 Int)
+ [ad +] [sb -] [mu *])
+
+(define (f/sub1 [x : X] #:where (Num2 X) -> X)
+ (ad x x))
+#;(typecheck-fail ; fails
+ (define (f/sub2 [x : X] #:where (Num2 X) -> X) (== x x))
+ #:with-msg "Body has type Bool, expected/given X")
+(define (f/sub2 [x : X] #:where (Num2 X) -> Bool)
+ (== x x))
+
+(check-type f/sub1 : (=>/test (Num2 X) (→ X X)))
+(check-type f/sub2 : (=>/test (Num2 X) (→ X Bool)))
+
+(check-type (f/sub1 1) : Int -> 2)
+(typecheck-fail (f/sub1 #f) #:with-msg "\\(Num2 Bool\\) instance undefined")
+(check-type (f/sub2 1) : Bool -> #t)
+(typecheck-fail (f/sub1 #f) #:with-msg "\\(Num2 Bool\\) instance undefined")
+
+(define-instance (Num2 Float)
+ [ad fl+] [sb fl-] [mu fl*])
+
+(define (square3 [x : X] #:where (Num2 X) -> X)
+ (mu x x))
+(check-type (square3 5) : Int -> 25)
+(check-type (square3 2.5) : Float -> 6.25)
+(define (memsq2? [x : X] [xs : (List X)] #:where (Num2 X) -> Bool)
+ (member? (square3 x) xs))
+(check-type (memsq2? 1 (list 1)) : Bool -> #t)
+(check-type (memsq2? 2 (list 2)) : Bool -> #f)
+(check-type (memsq2? 2 (list 3 4)) : Bool -> #t)
+(typecheck-fail (memsq2? (list 1) (list (list 1)))
+ #:with-msg "\\(Num2 \\(List Int\\)\\) instance undefined")
+(typecheck-fail (memsq2? #f (list #f))
+ #:with-msg "\\(Num2 Bool\\) instance undefined")
+
+(define-typeclass (Top X)
+ [fun1 : (→ X X X)])
+(define-typeclass (Top X) => (Left X)
+ [fun2 : (→ X X X)])
+(define-typeclass (Top X) => (Right X)
+ [fun3 : (→ X X X)])
+(define-typeclass (Left X) (Right X) => (Bottom X)
+ [fun4 : (→ X X X)])
+
+(define-instance (Top Int)
+ [fun1 +])
+(define-instance (Left Int)
+ [fun2 +])
+(define-instance (Right Int)
+ [fun3 +])
+(define-instance (Bottom Int)
+ [fun4 +])
+(define (left-fun2 [x : X] #:where (Left X) -> X)
+ (fun2 x x))
+(check-type (left-fun2 6) : Int -> 12)
+(define (left-fun1 [x : X] #:where (Left X) -> X)
+ (fun1 x x))
+(check-type (left-fun1 6) : Int -> 12)
+(define (bott-fun4 [x : X] #:where (Bottom X) -> X)
+ (fun4 x x))
+(check-type (bott-fun4 5) : Int -> 10)
+(define (bott-fun3 [x : X] #:where (Bottom X) -> X)
+ (fun3 x x))
+(check-type (bott-fun3 5) : Int -> 10)
+(define (bott-fun2 [x : X] #:where (Bottom X) -> X)
+ (fun2 x x))
+(check-type (bott-fun2 5) : Int -> 10)
+(define (bott-fun-Int [x : Int] -> Int)
+ (fun1 x x))
+(check-type (bott-fun-Int 5) : Int -> 10)
+;; lookup more than one parent level
+(define (bott-fun1 [x : X] #:where (Bottom X) -> X)
+ (fun1 x x))
+(check-type (bott-fun1 5) : Int -> 10)
+
+;; non-base typeclass instances with subclassing
+(define-instance (Top X) => (Top (List X))
+ [fun1 (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> l2]
+ [((x :: xs),(y :: ys)) -> (cons (fun1 x y) (fun1 xs ys))]
+ [_ -> l1]))])
+(define (top-list-fun1 [xs : (List X)] #:where (Top X) -> (List X))
+ (fun1 xs xs))
+(check-type (top-list-fun1 (list 5)) : (List Int) -> (list 10))
+(check-type (top-list-fun1 (list 5 6)) : (List Int) -> (list 10 12))
+
+(define-instance (Left X) => (Left (List X))
+ [fun2 (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> l2]
+ [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun2 x1 y1) (fun2 xs1 ys1))]
+ [_ -> l1]))])
+
+(define (left-list-fun2 [zs : (List X)] #:where (Left X) -> (List X))
+ (fun2 zs zs))
+(check-type (left-list-fun2 (list 6)) : (List Int) -> (list 12))
+(define (left-list-fun1 [xx : (List X)] #:where (Left X) -> (List X))
+ (fun1 xx xx))
+(check-type (left-list-fun1 (list 6)) : (List Int) -> (list 12))
+
+;; can use fun1 (from Top), for both X and (List X),
+;; in both instance def, and regular fns
+(define-instance (Right X) => (Right (List X))
+ [fun3 (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> l2]
+ [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun1 x1 y1) (fun1 xs1 ys1))]
+ [_ -> l1]))])
+(define (right-list-fun1 [xx : (List X)] #:where (Right X) -> (List X))
+ (fun1 xx xx))
+(check-type (right-list-fun1 (list 6)) : (List Int) -> (list 12))
+
+(define-instance (Bottom X) => (Bottom (List X))
+ [fun4 (λ ([l1 : (List X)] [l2 : (List X)])
+ (match2 (tup l1 l2) with
+ [(nil,nil) -> l2]
+ [((x1 :: xs1),(y1 :: ys1)) -> (cons (fun4 x1 y1) (fun4 xs1 ys1))]
+ [_ -> l1]))])
+
+;; lookup more than one parent level
+(define (bott-list-fun1 [xs : (List X)] #:where (Bottom X) -> (List X))
+ (fun1 xs xs))
+(check-type (bott-list-fun1 (list 5)) : (List Int) -> (list 10))
diff --git a/turnstile/examples/tests/rackunit-typechecking.rkt b/turnstile/examples/tests/rackunit-typechecking.rkt
@@ -11,7 +11,7 @@
(define (add-escs str)
(replace-brackets
(foldl (lambda (c s) (regexp-replace* c s (add-esc c))) str escs)))
- #;(define (expected tys #:given [givens ""] #:note [note ""])
+ (define (expected tys #:given [givens ""] #:note [note ""])
(string-append
note ".*Expected.+argument\\(s\\) with type\\(s\\).+"
(add-escs tys) ".*Given:.*"
diff --git a/turnstile/examples/tests/run-all-mlish-tests.rkt b/turnstile/examples/tests/run-all-mlish-tests.rkt
@@ -5,4 +5,5 @@
(do-tests "run-mlish-tests1.rkt" "General MLish"
"run-mlish-tests2.rkt" "Shootout and RW OCaml"
"run-mlish-tests3.rkt" "Ben's"
- "run-mlish-tests4.rkt" "Okasaki / polymorphic recursion")
+ "run-mlish-tests4.rkt" "Okasaki / polymorphic recursion"
+ "run-mlish-tests5.rkt" "typeclasses")
diff --git a/turnstile/examples/tests/run-mlish-tests5.rkt b/turnstile/examples/tests/run-mlish-tests5.rkt
@@ -0,0 +1,4 @@
+#lang racket/base
+
+;; adhoc polymorphism tests
+(require "mlish/generic.mlish")
