Be less dramatic about types

Author: masak

spec/08-types.md

@@ -7,11 +7,11 @@ than one type, but all values belong to at least one type. We say that a value
 A class is a form of type. Values are called _instances_ if they belong to a
 class.
 
-An interface is a form of type. If `v` is an instance of class `C`, which
-implements interface `I`, then `v is I` gives a truthy result.
+Interfaces are types. If `v` is an instance of class `C`, which implements
+interface `I`, then `v is I` gives a truthy result.
 
-An enum is a form of type. An enumeration constant `E.e` belongs to exactly one
-enum `E`, namely the one it was declared in.
+Enums are types. An enumeration constant `E.e` belongs to exactly one enum `E`,
+namely the one it was declared in.
 
 The built-in types `Int`, `Str`, `Bool`, `Array`, `Dict`, `Set`, `Bag`, and
 `Map` are also types.
@@ -20,25 +20,14 @@ Types exist both at compile time and at runtime. The declaration forms for
 classes, interfaces, and enums make sure to make the newly declared type
 available at compile time. Declaring a variable or parameter or return value to
 be of a given type is also a compile-time notion. The expression occurring on
-the left of a colon (`:`) in a declaration must be constructible at compile
-time so that the compilation can see it and make use of it.
+the left of a colon (`:`) in a declaration must be available at compile time so
+that the compilation can see it and make use of it.
 
 On the other hand, all the core features of Alma are guaranteed to work without
 such type annotations. Alma is a dynamically typed language, in the sense that
 the program needs to be well-formed syntactically and with respect to scoping
-in order to run, but does _not_ need to pass any checks made by the type
-inference algorithm. The adage "well-typed programs do not go wrong" reminds us
-that when a (sound) type-checker has given our program its blessing, certain
-classes of runtime error are ruled out. Alma has good support for static typing
-in the sense that Alma's type-checker provides the same guarantee -- but you're
-not prevented from running the program absent this guarantee, it's just that
-you do so with the understanding that those runtime errors are not ruled out.
-
-As a rule, it's safe to think of the program as existing on a level separate
-from the type annotations, and having meaning independently of them. Type
-annotations are fully aware of the program, but the program is not aware of
-type annotations, and cannot change its behavior based on what the type
-annotations say. Gilad Bracha calls this a _pluggable type system_.
+in order to run, but does _not_ need to pass any checks made as part of type
+inference.
 
 ## 6.1 Array types