The Theory of Types
By Richard Weyhrauch

This note is called: [TYPES]
The notations used in this note is described in [NOTATION]
Under development

Introduction

Remember our goal:

GOAL: to build an artifact that can think

Types are the things that we postulate as the mental images in the head of or thinking artifact. We use the word 'type' in the sense of 'what type of thing is this'. We imagine that every thing in our 'head' is a type.

There are many way to specify types in IBML.

One large group of types are determined by their attributes. One way we write these is

[l₁:v₁, ... ,l_n:v_n]

These types are the simplest to describe but are limited in their definability. But this needs

 

Types by recognizers

  + parts

  Finite sets
    Enumerations
  Comprehension Terms

  Recognizers


Define 
  attributes
  properties
  sorts

  recognizers - programs that tell us if an 'object' is of a certain 'sort'
   (FORALL obj (r [recognizer]) (eq (r obj) 'Yes) (eq (s obj) 'No))

 (|type| [1] |subtype| [natnum]
   (|def| 
     (*finite-set* @ (1))
   )
 )

Here Goes (currently nonesense)

  Requires <Tsys0 Csys0 Fsys0>

    (|type| [color] |subtype| [property]
     (|def| 
      (in-db |color|)
     ) )

    (COLOR? |red|)

    (type [red-object] subtype [object]
     (|def| (recognizer
      (lam (obj) (DATA-EQUAL (color-of obj) |red|) )) )

    a red ball
      (EXAMPLE |ball| [ball])
    a red ball - RED?([ball])  [ball is a subtype of [red]
    the ball is red - color(|ball|) = |red|

    (forall obj (iff (NAME? obj) (isin obj [name])
    (forall context term (if (TERM? term context) 
                             (if (isin term [name])
                                 (equal (apply #'name term) :TRUE) ) ) )


  Tsys0 (Scalers) 
    [TypeName] == {[answer] [character] [string] [symbol] [tag] [number] [host]  ... } 
    [typeDesc] == Or[ [TypeName] ...]

  Csys0
    #'dmop-symbol  = #dmop[#'bam-symbol]
    #'dmop-string  = #dmop[#'bam-string]
    #'dmop=integer = #dmop[#'bam-integer]

  Fsys0
    [language]
      [sortsym]
        (TypeName Example Isin Subtype)
            ... )
      [relsym]
        (TypeName Example Isin Subtype)
            ... )
      [funsym]
        ( (typeOf(typename obj))
      [indsym]
        ( ([object] Object () obj ... )
          ([integer] Integer (|1| |2| |3| ... ) i j n int ... )
          ([string] String str ... )
          ([symbol] Symbol sym ... )
          (1 2 3 ... ) 
           ... )
    [simulation-strucrure] 
      [computation-system]
        [reltation-system]
1111  [sort]
ation]( #'object #'integer #'symbol #'string ... )
        ()
        (#'typename #'example #'isin #'subtype)
    [facts]
      [fact]


      Subtype([integer],[object]) 
      Subtype([string],[object]) 
      Subtype([symbol],[object]) 
      Subtype([integer],[object]) 
      (forall o)(Example(o,[integer]) <=> Integer(o) )


  Tsys1
                   '[TypeName] '[TypeDef] '[TypeDesc] }
    [TypeDef] == List1[ [TypeName] [TypeDesc] ]
    [TypeDesc] == thingsRecognizedBy[#typename

    #'symbol = (lambda ((x [example])) apply(#'dmop x))

    
    [AtomicTypeDesc] == {'[integer] '[string] '[symbol] ...  } < SetOf[symbol]


    (forall (x [TypeDef])(if FiniteSetDefinition(x) then 
       #'recognizer-of(typeName(x)) = #'(program ((x [TypeDef])) #'setMember(x,#'setOf(x))) ) )  

    [IDKvalue] == { :IDK } 
    [BooleanValue] == { :True :False } 
    [RecognizedValue] == Union[ [BooleanValue] [IDKvalue] ]

  AtomicType 
    [integer] == thingsRecognizedBy[#'integer]
    Recognizer(#'integer)                                             ; requites  apply(#'integer,x) )          ; requires 
       ...



 [BaseTreeType] == ListOf[ List2[ [label] [BasicType] ] ] > [alist]
  [BaseType] == Or[ [AtomicTypeDesc]  [BaseTreeType] ] 

  

  [BaseExample] == Union[ [integer] [string] [symbol] ...  ] 


  [TypeDecs] = Or[ [BaseTypeDesc] 

  [TypeTree] == Or[ [BasicExample] [TypeDesc] ]

  [SYmbolTableEntry] ==- Tuple2[ [TypeName] [TypeDesc] ] 

  #'recognizer
  Or[ ]
  OneOf[ ]
  List1 ... list5 
  ListOf
  FiniteSet
  Alist
 

Axioms

 recognizer() = 

 recognizer([boolean]) = (lambda (x) (if (member x '(:True :False)) :True :False))
 recognizer([integer]) = (lambda (x) (if (integerp x) :True :False))
 recognixer([string])  = (lambda (x) (if (stringp x) :True :False))
 recognixer([symbol])  = (lambda (x) (if (symbolp x) :True :False))

 
  Theory of Types
  A Type theory

----------------------------------------

Parameterizad sexp types (sort of like backquote)

Example

  We write 
    `( ,[integer] ,[string] ) 
  to be the collection if lists where for each list,
    l ex  '( ,[integer] ,[string] )  <==>

  we have
   length(l)=2
   Integer(1st(l)) or [integer](1st(l)) or 1st(l) ex [integer]
   String(2nd(l)) or [string](2nd(l)) or 2nd(l) ex [string]

 and 

  if subtype(i,[integer]) and subtype(s,[string]}
    then
  subtype( `(,i ,s) `(,[integer] ,[string]) )

   :=  |
                 , |
                 ,@ |
                 ListOf[]
   := `ListOf[]

Union types

if t_1 t_n are [type-desc] then 
   union[[type-name(t_1)],...,[type-name(t_n)]] is a [type-desc]


if t_s subtype t-i then

 union[[type-name(t_1)],...,[type_name(t_s)],...,type-name(t_n)]]
   subtype
 union[[type-name(t_1)],...,[type_name(t_i)],...,type-name(t_n)]]

and

if x isin t_i then

   x isin union[[type-name(t_1)],...,[type_name(t_i)],...,type-name(t_n)]]