Pie

Backlinks

• Constructor (Pie)
  • In Pie, an expression is normal if it has a constructor on the top and all constructor's arguments are also normal
• An expression is normal if it has a constructor on the top with normal arguments
  • In Pie, an expression is normal if it has a constructor on the top and all constructor's arguments are also normal
• Pie is guaranteed to be total
  • Pie is guaranteed to be total - that is, every expression can be evaluated to find a value, no exceptions.
• A type has normal form
  • In Pie a Type has a normal form just like any other expression would. A type is the same as another type if they share the same normal form.
• A type is the same as another type if they share a normal form
  • In Pie, any two Types which share the same normal form are the same type. They are effectively isomorphic. Therefore
• The normal form of an expression is determined by the type of the expression
  • Because the normal form of an expression has a constructor for a type on top, asking for the normal form of an expression without a Type is meaningless in Pie. It isn't possible to normalise anything without type information.
• Pie cannot use recursion
  • Because Pie is guaranteed to be total, general recursion cannot be used. Some forms of simple recursion are allowed when they can be made to be total, however.