{"size": 1911, "ext": "scrbl", "max_stars_repo_path": "scribblings/controllable-refinement.scrbl", "max_stars_repo_name": "dannypsnl/controllable-refinement", "max_stars_repo_stars_event_min_datetime": "2020-10-22T05:04:31.000Z", "max_stars_repo_stars_event_max_datetime": "2020-11-20T11:19:50.000Z", "max_issues_repo_path": "scribblings/controllable-refinement.scrbl", "max_issues_repo_name": "dannypsnl/controllable-refinement", "max_issues_repo_issues_event_min_datetime": "2020-10-22T14:34:09.000Z", "max_issues_repo_issues_event_max_datetime": "2020-12-15T16:48:56.000Z", "max_forks_repo_path": "scribblings/controllable-refinement.scrbl", "max_forks_repo_name": "dannypsnl/controllable-refinement", "max_forks_repo_forks_event_min_datetime": null, "max_forks_repo_forks_event_max_datetime": null}
{"max_stars_count": 4, "max_issues_count": 7, "max_forks_count": null, "avg_line_length": 23.8875, "max_line_length": 328, "alphanum_fraction": 0.5996860283}
#lang scribble/manual
@require[@for-label[racket/base]
         scribble-math]

@title{controllable-refinement}
@author{Lîm Tsú-thuàn}

The type system based on @bold{STLC}, introducing user-controllable type refinement. Meta type variables are @${A}, @${B}. Meta predicate variable is @${P}. A type with predicate write as @${A_P}, introduce predicate write as @${P_+}, eliminate write as @${P_-}, @${P_{?+}} for anyway introduce, @${P_{?-}} for anyway eliminate.

@itemlist[
@item{verify-predicate @$${
\frac{
    \Gamma , f : A_{P} \rightarrow B , x : A_{P}
}{
    f x : B
}
}}

@item{introduce-predicate @$${
\frac{
    \Gamma , f : (p : A_{P_{+}}) \rightarrow B , x : A
}{
    f x : B , x : A_{P}, p : A
}
}}

@item{eliminate-predicate @$${
\frac{
    \Gamma , f : (p : A_{P_{-}}) \rightarrow B , x : A_{P}
}{
    f x : B , x : A , p : A_{P}
}
}}

@item{anyway-introduce-predicate @$${
\frac{
    \Gamma , f : A_{P_{?+}} \rightarrow B , x : A
}{
    f x : B , x : A_{P}
}
\frac{
    \Gamma , f : A_{P_{?+}} \rightarrow B , x : A_{P}
}{
    f x : B , x : A_{P}
}
}}

@item{anyway-eliminate-predicate @$${
\frac{
    \Gamma , f : A_{P_{?-}} \rightarrow B , x : A_{P}
}{
    f x : B , x : A
}
\frac{
    \Gamma , f : A_{P_{?-}} \rightarrow B , x : A
}{
    f x : B , x : A
}
}}
]

Notice that it can be extended to with polymorphism without changing previous definition.

@section{extension: related predicate}

Sometime we would like to update related predicate, for example:

@racketblock[
(: open (-> (file {writable readable})))
(: write (-> (file {writable}) void))
(: close (-> (file {+close}) void))

(let ([file (open "xxx")])
  (write file "hello")
  (close file)
  (write file "hello")) ;;; error
]

where @code{+close} also means @code{?-readable ?-writable}. This extension is quite simple, we can add related predicate information into environment, rewrite predicates of type while parsing type.
