(* Figure 7: production κ, ι *)
Inductive Kind : Type :=
- | KindType : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *)
- | KindTypeFunction : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
+ | KindStar : Kind (* ★ - the kind of coercions and the kind of types inhabited by [boxed] values *)
+ | KindArrow : Kind -> Kind -> Kind (* ⇛ - type-function-space; things of kind X⇛Y are NOT inhabited by expressions*)
| KindUnliftedType : Kind (* not in the paper - this is the kind of unboxed non-tuple types *)
| KindUnboxedTuple : Kind (* not in the paper - this is the kind of unboxed tuples *)
- | KindArgType : Kind (* not in the paper - this is the lub of KindType and KindUnliftedType *)
- | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *).
+ | KindArgType : Kind (* not in the paper - this is the lub of KindStar and KindUnliftedType *)
+ | KindOpenType : Kind (* not in the paper - kind of all types (lifted, boxed, whatever) *)
+ .
Open Scope string_scope.
Fixpoint kindToString (k:Kind) : string :=
match k with
- | KindType => "*"
- | KindTypeFunction KindType k2 => "*=>"+++kindToString k2
- | KindTypeFunction k1 k2 => "("+++kindToString k1+++")=>"+++kindToString k2
+ | KindStar => "*"
+ | KindArrow KindStar k2 => "*=>"+++kindToString k2
+ | KindArrow k1 k2 => "("+++kindToString k1+++")=>"+++kindToString k2
| KindUnliftedType => "#"
| KindUnboxedTuple => "(#)"
| KindArgType => "??"
end.
Instance KindToString : ToString Kind := { toString := kindToString }.
-Notation "'★'" := KindType.
-Notation "a ⇛ b" := (KindTypeFunction a b).
+Notation "'★'" := KindStar.
+Notation "a ⇛ b" := (KindArrow a b).
Instance KindEqDecidable : EqDecidable Kind.
apply Build_EqDecidable.
Fixpoint kind2latex (k:Kind) : string :=
match k with
- | KindType => "\star"
- | KindTypeFunction KindType k2 => "\star\Rightarrow "+++kind2latex k2
- | KindTypeFunction k1 k2 => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
+ | KindStar => "\star"
+ | KindArrow KindStar k2 => "\star\Rightarrow "+++kind2latex k2
+ | KindArrow k1 k2 => "("+++kind2latex k1+++")\Rightarrow "+++kind2latex k2
| KindUnliftedType => "\text{\tt{\#}}"
| KindUnboxedTuple => "\text{\tt{(\#)}}"
| KindArgType => "\text{\tt{??}}"
right; auto.
Defined.
-Definition tyConKind' tc := fold_right KindTypeFunction ★ (tyConKind tc).
+Definition tyConKind' tc := fold_right KindArrow ★ (tyConKind tc).
(* types prefixed with "Raw" are NOT binder-polymorphic; they have had their PHOAS parameter instantiated already *)
Section Raw.
:= fun TV env => σ TV env (cv TV env).
Definition HaskBrak {Γ}(v:HaskTyVar Γ ★)(t:HaskType Γ ★) : HaskType Γ ★:=
fun TV env => @TCode TV (TVar (v TV env)) (t TV env).
-Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindTypeFunction ★ (tyConKind tc))
+Definition HaskTCon {Γ}(tc:TyCon) : HaskType Γ (fold_right KindArrow ★ (tyConKind tc))
:= fun TV ite => TCon tc.
Definition HaskAppT {Γ}{κ₁}{κ₂}(t1:HaskType Γ (κ₂⇛κ₁))(t2:HaskType Γ κ₂) : HaskType Γ κ₁ :=
fun TV ite => TApp (t1 TV ite) (t2 TV ite).
Fixpoint caseType0 {Γ}(lk:list Kind) :
IList _ (HaskType Γ) lk ->
- HaskType Γ (fold_right KindTypeFunction ★ lk) ->
+ HaskType Γ (fold_right KindArrow ★ lk) ->
HaskType Γ ★ :=
match lk as LK return
IList _ (HaskType Γ) LK ->
- HaskType Γ (fold_right KindTypeFunction ★ LK) ->
+ HaskType Γ (fold_right KindArrow ★ LK) ->
HaskType Γ ★
with
| nil => fun _ ht => ht