rillian
/
rust-prehistory


			
							123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160
							

We'd like pieces of code to be reifiable, synthesizable, and
re-absorbable. Including types.

How?

   dyn -- a (value,type) pair, plus an operator to dyn-ify any typed value
   typecase -- ability to switch out of a dyn
   type comparisons -- ability to compare 2 unknown types
   type reification -- ability to traverse and analyze a type term
   
   ast -- representatives of all rust terms
   reify -- operator to turn a value into its ast
   quote -- syntax extension for entering literal asts
   env -- ability to reify the current environment
   mask -- separating off sections of the environment?
   eval -- operator to absorb an ast into an environment

What does it mean for a value to have a type?

   Structure of types. Literally: telling the runtime how to traverse
   the structure of the object.  Which bits to consider as pointers
   vs. integers vs. container-parts.

   In a variable stored in a static environment -- say an activation
   frame -- the frame stores a pointer to its code value, and that
   code value stores a frame layout description, including the types
   of all the slots. No problemo.

   If I pass a dyn to you, you have no idea what the type of the thing
   is. Your frame has no idea.  So I have to pass the type with the
   value.

   Should the type be separable? Sure, why not? Suppose I want to run
   a function to perform some calculation on the type alone. Might as
   well be possible.

What difficulties arise when traversing a type?

   If I hit a named subterm, I have to look it up (or it can be
   expanded inline, if it's acyclic)

   Suppose I package a type by saying "here is an environment with N
   terms, and the one we're talking about is term K in this
   environment". Is that useful? Practical?

   The environment can carry a minimal set of terms, rather than say
   an entire module of unrelated terms. This is useful in a
   compatibility sense: types T and V are equal when their minimal
   dependency environments are equal?

Working from slightly modified napier88 design: system should be
persistable (not persistent). That is: every running program should
serialize in a way that is both sensibly de-serializable *and* can be
massaged into working / being interpreted in a future context.
Persistence of data should, in other words, not prevent *evoution* of
the system.

How?

Napier decided to do structural typing, on the basis that the bindings
from types to environments became basically irrelevant: types are
closed terms in this model, and with a little bit of clever
hash-consing and care to chose normalizing forms, you don't need to
worry about which environment a type gets defined in. This is very
helpful in evolving the system.

The napier docs are concerned that combining universal quantifiers and
recursive structural types leads to undecidable equivalence, for
example they give this term:

  type anyarr[T] = variant { simple: t, complex: anyarr[array[T]] }

They claim this is not decidable. Why? Hmm. Because anyarr[T] expands
at each unfolding rather than contracting or remaining constant,
i.e. the checking process potentially diverges? Well, it's a messy
term anyways. One way or another -- we need to find the rationale! --
they add a restriction that supposedly recovers decidability:

  The specialisation of a recursive operator on the right hand side of
  its own definition may not include any types which are constructed
  over its own formal parameters.

IOW the term has to contract. These are ok:

     type x[T] = ... x[T] ... 
     type x[T] = ... x[Y] ...

but this is not:

     type x[T] = ... x[foo[x[T]]]

That's fine. Let's assume we have to use that too for now.

Persistence! I want to think about this and be clear about it. Rust
modules should be persistable.


  level 0 encoding: the elias omega octet code
  level 1 encoding: the code numbers for a file:

     "Rust"   : ascii < omega-octets, so just |0x52 0x75 0x73 0x74| 
     <vers>   : a version number (hint), we start with 0
     <body>   : an artifact constructed from a grammar!

        type terms:

          hw types
          ---------------------- 
           s<N>
           u<N>
           flo = ieee754.bfp
           dec = ieee754r.dfp

          prim types
          ---------------------- 
           nil
           bool
           int
           char = unicode5.codepoint
           str = unicode5.utf8_nfc
           prog
           proc

          dynamics
          ----------------------
           dyn
           env (is this required? merely a napier idiom, or deep issue?)           

          anonymous constructors
          ----------------------
           vec[]
           tup[]
           abs[]
           func[]()->
           func?[]()->
           func![]()->
           func*[]()->
           func+[]()->
           port[]()->
           port?[]()->
           port![]()->
           port*[]()->
           port+[]()->
           chan[]()->
           chan?[]()->
           chan![]()->
           chan*[]()->
           chan+[]()->

          labeling constructors
          ---------------------- 
           rec{}
           alt{}

          AST nodes:
          ...