johnchandlerburnham

package example_contract
  open introit
  open contract
  lang contract
where

// pure datatypes are defined outside of contracts
data SimpleToken {
  value: Integer,
  mintedBy: Address,

johnchandlerburnham

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE MultiWayIf #-}
module Wau where

import           Data.Map                       (Map)
import qualified Data.Map                       as M
import           Data.Maybe                     (isJust)
import           Data.Set                       (Set)
import qualified Data.Set                       as Set
import           Data.STRef

johnchandlerburnham

W(A : Type, B : A -> Type) : Type
  w<P : W(A,B) -> Type> ->
  (sup : (x: A, f: B(x) -> W(A,B)) -> P(W.sup<A,B>(x,f))) ->
  P(w)

W.sup<A: Type, B: A -> Type>(x: A, f: B(x) -> W(A,B)) : W(A,B)
  <P> (sup) sup(x,f)

T Two
| t0;

johnchandlerburnham

We start with a scope (list of names and types n : T) and a specific type A as our goal.

Initial Scope:

f : C -> B
g : D -> B -> A
h : C
i : D

johnchandlerburnham

// Standard construction of Matrix based on Vector
//T Matrix <A: Type> ~ (rows: Nat, cols: Nat)
//| matrix<rows:Nat,cols:Nat>(vecs: Vector(Vector(A,cols),rows)) ~ (rows,cols);

Matrix(A: Type, n: Nat, m: Nat) : Type
  matrix<P: (n: Nat) -> (m: Nat) -> Matrix(A,n,m) -> Type> ->
  (znil: P(Nat.0,Nat.0,Matrix.znil<A>)) ->
  (rnil: P(Nat.1,Nat.0, Matrix.rnil<A>)) ->
  (cnil: P(Nat.0,Nat.1, Matrix.cnil<A>)) ->
  (cell: (x : A) -> P(Nat.1,Nat.1, Matrix.cell<A>(x))) ->

johnchandlerburnham

I: Type
  i<P: (i:I) -> Type> ->
  (I0: P(I.0)) ->
  (I1: P(I.1)) ->
  (IE: Path(P, I0, I1)) ->
  P(i)

I.0: I
  <P> (i0) (i1) (ie) i0

johnchandlerburnham

// To type-check, install npm:
// $ curl -o- https://raw.githubusercontent.com/nvm-sh/nvm/v0.35.3/install.sh | bash
// $ nvm install 13.10.1
// 
// Then install Formality-Core:
// $ npm i -g formality-core
//
// Then download this file:
// $ curl https://gist.githubusercontent.com/MaiaVictor/28e3332c19fbd80747a0dceb33896b6b/raw/ae8d798225d2e6cc600e158f27d1b83ff384c262/intervals_with_self_types.fmc.c >> main.fmc
//

johnchandlerburnham

Arcsec : (S : Type) -> (E : Type) -> (A: Type) -> Type
  (S) (E) (A)
    <B : Type> ->
    Parsec.State(S)(E) ->
    (Bool -> Parsec.State(S)(E) -> Either(Parsec.Error(E))(A) -> B) ->
    B

Arcsec.Reply : Type -> Type -> Type -> Type
  (S) (E) (A)
  arcsec_reply<P: Arcsec.Reply(S)(E)(A) -> Type> ->

johnchandlerburnham

A Taxonomy of Self-Types

Part I: Introduction to Self-Types

Datatypes in the Formality programming language are built out of an unusual structure: the self-type. Roughly speaking, a self-type is a type that can depend or be a proposition on it's own value. For instance, the consider the 2 constructor datatype Bool:

johnchandlerburnham

// Parse.test : String
// Parse.parse<String>
// | Parse.tokens("a");
// | "a";

module.exports = (function (){
  var F64 = new Float64Array(1);
  var U32 = new Uint32Array(F64.buffer);
  var F64_get = (x,i)=>((F64[0]=x),(i<32?(U32[0]>>>i)&1:(U32[1]>>>(i-32)&1)));
  var F64_set = (x,i)=>((F64[0]=x),(i<32?(U32[0]=U32[0]|(1<<i)):(U32[1]=U32[1]|(1<<(i-32)))),F64[0]);