Formality functional programming language

xholonWorkbook.xml

<?xml version="1.0" encoding="UTF-8"?>
<!--Xholon Workbook http://www.primordion.com/Xholon/gwt/ MIT License, Copyright (C) Ken Webb, Sun Mar 08 2020 14:37:13 GMT-0400 (Eastern Daylight Time)-->
<XholonWorkbook>

<Notes><![CDATA[
Xholon
------
Title: Formality functional programming language
Description: 
Url: http://www.primordion.com/Xholon/gwt/
InternalName: 0c265f43c8ef8af017bb479ec21cd141
Keywords: 

My Notes
--------
March 8, 2010

flipper.fm (Formality example, from ref[3])
----------
// Save it as flipper.fm, install Formality and type this in the same directory:
// fm -J flipper/@

// Bit type
T Bit
| b0
| b1

// Flips a bit once
flip_once(bit: Bit) : Bit
  case bit
  | b0 => b1
  | b1 => b0

// Flips a bit many times
flip_times(times: Number, bit: Bit) : Bit
  if times === 0 then
    bit
  else
    flip_times(times - 1, flip_once(bit))

// The Equal type from Base lib, since we didn't import it
T Equal{A, a : A} (b : A)
| equal : Equal(A, a, a)

// For any bit, flipping it twice returns itself
MyTheorem(bit: Bit) : Type
  flip_times(2, bit) == bit

// Proof of the statement above
my_proof(bit: Bit) : MyTheorem(bit)
  case bit
  | b0 => equal(__)
  | b1 => equal(__)
  : MyTheorem(bit)


References
----------
(1) https://github.com/moonad/Formality
    An efficient proof-gramming language.

(2) https://github.com/moonad/Formality/blob/master/DOCUMENTATION.md

(3) https://medium.com/@maiavictor/the-refreshing-simplicity-of-compiling-formality-to-anything-388a1616f36a
    The refreshing simplicity of compiling Formality to anything
    Victor Maia, Feb 14, 2020 · 5 min read
    Formality is a new programming language featuring theorem proving that, unlike most in the category, is designed to have a familiar syntax and run efficiently.
    I often associate it with “optimal interaction-net runtimes” that outperform Haskell, Ocaml, Clojure and other functional languages in some very high-order algorithms.
    KSW has flipper.fm example, that works after I fix in few errors in the names of variables in the supporting JS code

(4) https://medium.com/@maiavictor/introduction-to-formality-part-1-7ae5b02422ec
    Introduction to EA Type Theory - Whys, installation, simple types/programs/proofs
    Victor Maia, Apr 22, 2019 · 14 min read

(5) https://medium.com/@maiavictor/solving-the-mystery-behind-abstract-algorithms-magical-optimizations-144225164b07
    Solving the mystery behind Abstract Algorithm’s magical optimizations
    Victor Maia, Aug 16, 2018 · 13 min read

]]></Notes>  

<_-.XholonClass>
  <PhysicalSystem/>
  
  <FmFlipper/>
  <FmSum/>
  
</_-.XholonClass>

<xholonClassDetails>
  <Avatar><Color>red</Color></Avatar>
</xholonClassDetails>

<PhysicalSystem>
  <FmFlipper/>
  <FmSum/>
</PhysicalSystem>

<FmFlipperbehavior implName="org.primordion.xholon.base.Behavior_gwtjs"><![CDATA[
// Formality functional programming language
// example from medium.com article
// this is JavaScript, compiled from the .fm file, using (on my computer):
// cd ~/nodespace/Formality
// fm -J flipper/@
var flipper = (function(){
  var _flipper$Bit = undefined;
  var _flipper$b0 = (_0=>(_1=>_0));
  var _flipper$b1 = (_0=>(_1=>_1));
  var _flipper$flip_once = (_0=>_0(_flipper$b1)(_flipper$b0));
  var _flipper$flip_times = (_0=>(_1=>((_0===0? 1 : 0)?_1:_flipper$flip_times((_0-1))(_flipper$flip_once(_1)))));
  var _flipper$Equal = (_0=>(_1=>(_2=>undefined)));
  var _flipper$equal = (_0=>_0);
  var _flipper$MyTheorem = (_0=>_flipper$Equal(undefined)(_flipper$flip_times(2)(_0))(_0));
  var _flipper$my_proof = (_0=>_0(_flipper$equal)(_flipper$equal));
  return {
    'Bit':_flipper$Bit,
    'b0':_flipper$b0,
    'b1':_flipper$b1,
    'flip_once':_flipper$flip_once,
    'flip_times':_flipper$flip_times,
    'Equal':_flipper$Equal,
    'equal':_flipper$equal,
    'MyTheorem':_flipper$MyTheorem,
    'my_proof':_flipper$my_proof
  };
})()

// I had to fix a few names that were incompatible with the above function
this.println("Testing the Formality language - flipper");
var encode_bool = bool => True => False => bool ? True : False;
var decode_bool = bool => bool(true)(false);// Tests our algorithm
var times  = 101;
var bool   = encode_bool(true);
var result = flipper.flip_times(times)(bool);
var output = decode_bool(result);
this.println(output); // false

this.println(decode_bool(flipper.flip_times(2)(encode_bool(true)))); // true

/* more TESTING
flipper.flip_times(1)(encode_bool(true))
function _a$b1(_0)

flipper.flip_times(1)
function flip_times(_1)

decode_bool(flipper.flip_times(1)(encode_bool(true)));
false

decode_bool(flipper.flip_times(1)(encode_bool(false)));
true

decode_bool(flipper.flip_times(2)(encode_bool(true)));
true

*/
  //# sourceURL=FmFlipperbehavior.js
]]></FmFlipperbehavior>

<FmSumbehavior implName="org.primordion.xholon.base.Behavior_gwtjs"><![CDATA[
// Formality functional programming language
// example from Documentation.md
// this is JavaScript, compiled from the .fm file, using (on my computer):
// cd ~/nodespace/Formality
// fm -J sum/@
const {twice, vector_size, sum} = (function(){
  var _sum$twice = (_0=>(_0*2));
  var _sum$vector_size = (_0=>(_1=>(((_0**2)+(_1**2))**0.5)));
  var _sum$sum = (_0=>((_0===0? 1 : 0)?0:(_0+_sum$sum((_0-1)))));
  return {
    'twice':_sum$twice,
    'vector_size':_sum$vector_size,
    'sum':_sum$sum
  };
})()

this.println("Testing the Formality language - sum");
this.println(twice(3)); // 6
this.println(sum(1)); // 1
this.println(sum(4)); // 10
this.println(sum(10)); // 55
this.println(vector_size(3)(4)); // 5

/* more TESTING


*/
  //# sourceURL=FmSumbehavior.js
]]></FmSumbehavior>

<SvgClient><Attribute_String roleName="svgUri"><![CDATA[data:image/svg+xml,
<svg width="100" height="50" xmlns="http://www.w3.org/2000/svg">
  <g>
    <title>FmFlipper</title>
    <rect id="PhysicalSystem/FmFlipper" fill="#98FB98" height="50" width="50" x="25" y="0"/>
    <g>
      <title>FmSum</title>
      <rect id="PhysicalSystem/FmSum" fill="#6AB06A" height="50" width="10" x="80" y="0"/>
    </g>
  </g>
</svg>
]]></Attribute_String><Attribute_String roleName="setup">${MODELNAME_DEFAULT},${SVGURI_DEFAULT}</Attribute_String></SvgClient>

</XholonWorkbook>