;;; NOTE: This document is just a draft idea sketch pad

;;; Data types

; Resp uses algebraic datatypes which can also be used in an
; object based style with more flexibility than typical of
; languages with algebraic datatypes
;
; There is a single way of defining a type (the 'type' form) which
; encompasses unions, records, objects, etc.

; A type is a discriminated union ("or") of types.
; Type names (including variables) always start with an uppercase letter.

; There are many equivalent terms for kinds of types.  We uniformly use:
; "Union"  : "and", sum type
; "Record" : "or", product type, object, struct

; Example: A Tree is a Node with a value and left/right children, or Nothing
; "Nothing" and "Node" are called constructors.  In this case both are Records
(type (Tree T)
  (Nothing)
  (Node value :T
        left  :(Tree T)
        right :(Tree T)))

; Constructors have one of two forms:
; Union constructors have parameters enclosed in parenthesis, e.g.
;   (Maybe (Nothing) (Just x))
; Record constructors do not, e.g.
;   (Point x y)
;
; Thus, types can be arbitrarily combined/nested, e.g
(type (Collection T)
  (Tree
    (Nothing)
    (Node value :T
          left  :(Tree T)
          right :(Tree T)))
  (List
    (Nothing)
    (Node value :T
          next  :(List T))))

; Tree height (functional pattern matching style)
(def (height t)
  (match t:Tree
    (Empty) 0
    (Node v l r) (+ 1 (max (height l) (height r)))))

; equivalently
(def (height t)
  (match t
    (Tree.Empty) 0
    (Tree.Node v l r) (+ 1 (max (height l) (height r)))))

; GADTs
; The return type of a constructor can be specified explicitly
; e.g. a well-typed evaluator (this is not possible without GADTs):
; (http://www.haskell.org/ghc/docs/latest/html/users_guide/data-type-extensions.html#gadt)
(type (Term T)
  (Lit    i :Int)      :(Term Int)
  (Succ   t :Int)      :(Term Int)
  (IsZero t :Int)      :(Term Bool)
  (If     c :Bool
          t :(Term T)
          e :(Term T)) :(Term T)
  (Pair   a :(Term T)
          b :(Term T)) :(Term T))

; Objects
; A type with a single product constructor is simply that product type
; (i.e. sum types with a single element do not exist by definition)
; This can be used to create "record" or "object" types without any special
; language facilities:
(type (Person)
  (Person
    name :String
    age  :Number))

; The '.' ("dot") operator can be used to inspect product types

(def dave (Person 'name "Dave" 'age 27))

(. dave name) ; => "Dave"
(. dave age) ; => 27


;; Everything Is A ...

; Everything in Resp is a closure.  Records are simply closures with some
; internal definitions exposed (much like modules).

; Objects can be created with their constructors:
(def steve (Person "Steve" 24))

; Equivalently (aside from type) with the generic Object constructor:
(def steve2 (Object 'name "Steve" 'age 24))

; Equivalently (aside from type) manually:
(def steve2
  (fn ()
    (def name "Steve")
    (def age 24)
    (export name age)))

;; RDF style objects

; A class is just an object (closure) with some required properties (ala OWL)
; All object fields have a URI.  If a prefix is not explicitly given, the URI
; is the base URI of the document, followed by the Class, a dot, then the name.
; e.g. if the base URI of this document is "foo://bar/" the URI of "age" below is:
; foo://bar/Person.age

(ns foaf "http://xmlns.com/foaf/0.1/")
(ns geom "http://www.charlestoncore.org/ontology/2005/08/geometry")

(def (Point T)
  (Point
    geom.x :T
    geom.y :T))

(type (Person)
  foaf.name :String
  age       :Number)

(type (Cat)
  foaf.name :String
  age       :Number)

; A 'constructor' (nothing special, just a function that returns a closure)
(def (newborn name)
  (fn ()
    (def type Person) ; special, compiler will check required properties exist
    (def foaf.name name)
    (def age 1)))

; Equivalently,
(def (newborn name)
  (Person
    foaf.name name
    age       1))

(def stewie (newborn "Stewie"))
(def stewies-age (. stewie age))