# Advanced Redex Trails

# Advanced Redex Trails:

### limitations, bugs, and workarounds

This is a fuller list of limitations, bugs, and workarounds in the prototype tracing system, Hat. (There is also an overview page, and a more detailed page about the browser interface.) Please mail us at ART-team@cs.york.ac.uk to report any new limitations, bugs, and workarounds that you discover.

### Bugs and holes in the current trace compiler:

The traced program evaluates too much
  The traced program

  >     main = print (True || h True)

  >     h = h

  does not terminate. The reason is that the trace transformation assumes that all values of type R t are of the form R v Trace. In the example the Sat for h True has to be constructed (to be able to show the expression). h has value R h' (Nm "h"). Then h' is applied to R True (Nm "True"). However, h' has value bottom and hence the value of this application is also bottom, that is, is not of the form R v Trace.

  This program has the additinal problem that it cannot be interrupted with Control-C. Interruption is only possible when reduction of a traced application is entered, not such an internal, real application.

  >     main = print (True || h True True)

  >     h x = h x

  This does not terminate for the same reason as above. It can, however, be interrupted and finally runs out of heap.
Oversaturated applications are not shown correctly

  >     main = print ((h True) True)
  >     h x = f
  >     f x = False

  correctly gives `h True` as parent of `f` and `main` as parent of `f True`, but

  >     main = print (h True True)
  >     h x = f
  >     f x = False

  incorrectly gives `h True True` as parent of `f` and also of `f True`!

  Oversatured applications are handled completely the wrong way round by the transformation. There is no code to every create an App trace node for the saturated application `f True`.

Overloaded numeric constants all fixed
  literal Integers in patterns cause an "fsExp: strange expression" compiler error
  (fixed, August 2000)
  literal Ints/Integers in definitions cause an "fsExp: strange expression" compiler error
  (fixed, July 2000)
  literal floats cause an "overloaded rational" compiler error (fixed, August 2000)
Pattern bindings are projections but not handled as such
  Example:

  >     translateStatement symboltable startAddress (Assignment identifier exp)
  >         = (expCode ++ [Sto varAddress], expCodeLength+1)
  >         where
  >         (expCode, expCodeLength) = translateExpression symboltable startAddress exp
  >         Just varAddress = tableRead identifier symboltable

  The parent of the value of `varAddress` should be `tableRead ...`. Instead the parent is the parent of the object that was originally inserted into the table. Here definitely reductions are not recorded in the trail.
Strictness annotations in data type definitions
  are not transformed correctly. With tracing, the data constructor is no longer strict in an argument annotated with !. Example:

  >     data Test = T !Bool

  >     f (T x) = True

  >     t = error "Hello"

  >     main = print (f (T t))

  With tracing this program prints `True`, although it should abort with the error message `"Hello"`.
Type Synonyms
  Type synonyms for arrow types are not necessarily translated correctly. In fact, at the moment they are not translated at all.
newtype (fixed 18/8/00)
  A newtype often leads to a segmentation fault of the traced program. More precisely, pattern matching on the data constructor yields a nonsense value, probably a pointer is interpreted as data constructor. For example:

  >     newtype Test = T Int

  >     f (T x) = x

  >     main = print (f (T 3))

  yields `13493678`.
Higher-Order Types
  Data types with type variables of a kind beyond simple * cannot be handled by the transformation. Currently not even the normal nhc can handle them.

  When the latter problem is solved (or for a nhc independent version), the tracing transformation can be changed to handle higher-order type variables. We introduce a data type

  >     newtype Fun a b = Trace -> R a -> R b

  and the transformation replaces all `->`'s by `Fun`.
Records
  Records are currently not supported.
Derived Classes (fixed, July 2000)
  Derived classes do not work correctly. Hence read does not work when derived. It demands an instance of class Read for the tracing type R.
The cause is that data types are transformed for tracing before deriving. The order should be reversed.
Prelude and Libraries
  libraries Array, Directory, etc. missing
  functions readFile, appendFile are missing from library IO
  more generally, output IO is `special' because the tracer has to record it such that the user can later select trails from it. Thus, it is unclear what the meaning of many IO functions should be.
Unidentified bugs
  on one occasion the compiler stopped with No match in _dCaf
  on a few occasions the compiler crashed with heap overrun

### Bugs and holes in the run time system part for tracing

Our of heap space
  Currently also a tracing program just abort, if it runs out of heap space. It should connect to the browser instead. Probably the same problem occurs, if the program runs out of stack space.
Runtime system crashes

  >     Program exited normally.
  >     in_bind_ne: bindin_bind_ne: resolver error. Host = LOCAL
  >     in_bind_ne: in_bind RETURNED BAD VALUE: -1

  This seems to happen when the browser has just been started and may still be initialising, not yet able to communicate.

## Wishes

Trusting derived instances
  Currently derived instances have the same trusting status as the module in which they are derived. However, these instances should be trusted, because they are derived automatically. Possibly an additional compiler flag would permit to make these instances untrusted.

  The same applies to other compiler-generated code, e.g. to the automatically created selectors for field names.

This page last modified: 2001.01.17.