wiki:Language/Core/Variables

Variables and Constructors

Var        ::= NamedVar | IndexVar
NamedVar   ::= Lower VarChar* '#'?
IndexVar   ::= '^' Digit+

Con        ::= NamedCon | SymbolCon
NamedCon   ::= Upper VarChar* '#'? 
SymbolCon  ::= '~>' | '=>' | '->'

VarChar    ::= Lower | Upper | Digit | '_' | '\''  (prime)

Lower      -> (lower case letter)
Upper      -> (upper case letter)
Digit      -> (0 - 9) 

Variables can be named or bound via a deBruijn index. Named variables start with a lower case letter, and can be followed by upper and lower case letters, digits, underscores and primes. Index variables start with a hat and are followed by some digits.

Constructors can have textual or symbolic names. A textual constructor starts with an upper case letter, and can be followed by upper and lower case letters, digits, underscores and primes. Named constructors can optionally end with a hash.

  • DDC uses deBruijn indices internally when performing capture avoiding substitution, and to avoid needing to generate fresh names. deBruijn indices can also be used in source programs.
  • Names that end with a hash are used for primitive types and operators that are built in to the language fragment.

Built-in Constructors

The following constructors are baked into the ambient Disciple language, though not all can be used in all language fragments.

  • In the current implementation (DDC 0.4), the names of constructors that are not part of a particular language fragment cannot be reused for other purposes. For example, although the Tetra fragment does not include closure typing, we cannot re-use the name Closure in programs in that fragment. Built-in names that are not used in a particular language fragment should be treated as "reserved for future use".

Built-in Sort Constructors

Syntax
Prop
Comp

Sorts are the highest classifiers.

Built-in Kind Constructors

SyntaxSort
Data :: Comp
Region :: Comp
Effect :: Comp
Closure :: Comp
Witness :: Prop
(~>) (must be fully applied)
  • The kind arrow (~>) has arity-2 and must be fully applied. For example, both Data ~> Data and Region ~> Effect are well sorted.

Built-in Data Type Constructors

SyntaxKindDescription
Unit :: Data Unit data type constructor
S :: Effect ~> Data ~> Data Suspended computation constructor
(=>) :: Prop ~> Data ~> Data Function type constructor
:: Prop ~> Prop ~> Prop
(->) :: Data ~> Data ~> Data Witness type constructor
:: Data ~> Effect ~> Closure ~> Data ~> Data
  • The implication arrow (=>) can have two possible kinds, shown above.
  • The function arrow classifies a function that may diverge or perform some other effect when it is applied. The purity of the function space depends on the language fragment. The Tetra and Salt language fragments use standard function kind for the function cosntructor. The function constructor in the Eval and Lite language fragments also take an Effect and Closure parameter.

Built-in Effect Type Constructors

SyntaxKindDescription
Read :: Region ~> Effect Read effect on some region
HeadRead :: Data ~> Effect Read effect on the head region of some type.
DeepRead :: Data ~> Effect Read effect on all material regions in some type.
Write :: Region ~> Effect Write effect on some region
DeepWrite:: Data ~> Effect Write effect on all material regions in some type.
Alloc :: Region ~> Effect Allocation effect on some region.
DeepAlloc:: Data ~> Effect Allocation effect on all material regions in some type.

Build-in Closure Type Constructors

SyntaxKindDescription
Use :: Region ~> ClosureUse of some region.
DeepUse :: Data ~> ClosureUse of all material regions in some type.

Built-in Witness Type Constructors

SyntaxSpecDescription
Global :: Region ~> Witness Objects in global regions are allocated in the heap, instead of on local stacks.
DeepGlobal :: Data ~> Witness All material regions in some type are global.
Const :: Region ~> Witness Objects in constant regions cannot be destructively updated.
DeepConst :: Data ~> Witness All material regions in some type are constant.
Mutable :: Region ~> Witness Objects in mutable regions may be destructively updated.
DeepMutable :: Data ~> Witness All material regions in some type are mutable.
Lazy :: Region ~> Witness Lazy regions may contain thunks instead of manifest objects.
HeadLazy :: Data ~> Witness Head region in some type may contain thunks.
Manifest :: Region ~> Witness Manifest regions do not contain thunks.
Purify :: Effect ~> Witness Enforce purity of an effect.
Emptify :: Closure ~> Witness Enforce emptiness of a closure.
Disjoint :: Effect ~> Effect ~> Witness Effects are disjoint (commutable)
Distinct :: Region ~> Region ~> Witness Regions are distinct (effects on them are commutable

Built-in Data Constructors

SyntaxSpecDescription
() :: Data The unit value

History

  • 2013/04: Renamed symbolic kind constructors * % ! $ to Data Region Effect Closure respectively. We started using other abstract kind constructors like Rate for the Disciple Core Flow fragment, and having some kind constructors as symbols and some named variables looked too inconsistent.
  • 2011/12: Eliminated namespace prefixes on variables. Effect variables used to be written like !e1, while closure variables were written like $c1 etc.. The prefixes were eliminated because we felt that they cluttered the syntax too much. As core programs are usually generated by the compiler, there is no problem with choosing new names to avoid clashes.
  • 2011/12: Gave the kind arrow its own syntax ~> instead of reusing ->. Now that we use the same type grammar for both Spec and Kind, these needed to be disambiguated.
  • 2011/12: Renamed old Share and DeepShare constructors to Use and DeepUse. We're starting to think of closure terms like usage effects, which are masked by Global constraints instead of Const constraints.
  • 2011/12: Added Global and DeepGlobal constructors. Implementing the stand-alone core language makes region vs heap allocation easier to experiment with, even if we don't implement it in the compiler proper.
  • 2011/12: Added Alloc and DeepAlloc. We didn't use to track these, instead inferring partial allocation information from the region quantifiers on types. Using an allocation effect and separate purification rule seems cleaner.
Last modified 3 years ago Last modified on Mar 8, 2014, 6:38:23 AM