| import Base# | |
| // There are eight possible winning lines in a game of tic-tac-toe | |
| // ---------------- | |
| // | 00 | 01 | 02 | | |
| // -----+----+----- | |
| // | 10 | 11 | 12 | | |
| // -----+----+----- | |
| // | 20 | 21 | 22 | | |
| // ---------------- |
| module FiniteEndoTypes where | |
| import System.IO | |
| -- for any finite n, there are n^n mappings from the set with n elements to | |
| -- itself | |
| -- for n == 2 | |
| -- {0,1} -> {0,0} 0 | |
| -- {0,1} -> {0,1} 1 |
| Equal: (A: Type) -> A -> A -> Type | |
| (A) (a) (b) | |
| equal_value<P: (b: A) -> Equal(A)(a)(b) -> Type> -> | |
| (equal: P(a)(equal<A><a>)) -> | |
| P(b)(equal_value) | |
| equal: <A: Type> -> <a: A> -> Equal(A)(a)(a) | |
| <A> <a> | |
| <P> (equal) |
| // 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]); |
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:
| 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> -> |
| // 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 | |
| // |
| 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 |
| // 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))) -> |
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