Skip to content

Instantly share code, notes, and snippets.

@rinarakaki

rinarakaki/albino.md

Last active January 19, 2023 03:06
Show Gist options
  • Save rinarakaki/d46c09cebf354ce48c6c47cbfbef2379 to your computer and use it in GitHub Desktop.
Save rinarakaki/d46c09cebf354ce48c6c47cbfbef2379 to your computer and use it in GitHub Desktop.
Download ZIP
Albino language specification.
Raw
albino.md

Type

# 'none' is a value
none of None

# 'True' and 'False' are higher-order exists
True is not False
False is not True
# TODO 'True or False' looks evaluation. Can this be a justification of 'type' keyword?
type Bool = True or False

# Types are ordered by logical implication
# Incorrect statement raises error immediately
True is True or False  # Correct
True and False is True  # Correct
True or False is True  # Raises error (rather than returns 'False')

type Day = Mon or Tue or Wed or Thu or Fri or Sat or Sun
Mon is Day

# Named disjunction
type T = a of A or b of B

# Syntactic type definition
type Point = (I32, I32)  # Numbered, '(I32,)' when only an item
type Person = (name of String, age of I8)  # Named

# Operational (function) type
add(x of I8, y of I8) of I8 = x + y
add of I8(x of I8, y of I8)  # Correct

# Higher-order operational (function) type
I8(I8)(I8)  # TODO = (I8(I8))(I8) = I8((I8)(I8)) = I8(I8(I8)) ?

# TODO Python's indentation rule is made not only by indent and newline but also by ':'.

# Dependent type
# TODO Is this a statement on the type or the function 'x. x != 0'?
type Nonzero = I8 and not x = 0 for x of it

# IDEA
type Nonzero
    it is I8
    not x = 0 for x of it

type Set(items of (T, ...))
    ...
    
    it.add(item of T)
        ...

# There are type-level operations ('and', 'or', 'not', 'is') and value-level operations ('*', '+', '=').


# Evaluation

# 'if' statement is a type-level error handling
if a
    ...

# Judgement on if 'x' is of 'I8'
if x of I8 and not x = 0
    ...

# Structural judgement
point = (1, 2)
if point of Point  # Correct
    point(0) ** 2 + point(1) ** 2  # Refer the values by 'object(n)' or 'object::n'

person of Person = (name = 1, age = 30)  # Error: Type of 'name' should be 'String'.
person::name  # Refer the values by 'object.name' or 'object::name'.

# Literal processing
if 1 = 1  # Correct
    ...

if (1, 2) = (1, 2)  # Correct
    ...

# Assignment

Left side: without evaluation, literal
Right side: with evaluation


(a = x, b = (c = y)) = (a = 0, b = (c = 1))  # x, y = 0, 1

SomeType(x, y) = SomeType(0, 1)  # x, y = 0, 1

"Hello, {name}!" = "Hello, Me!"  # name = "Me"

Operation

Though Albino is , it has procedural aspect which is evoked by ':' like Haskell's 'do'. In Albino, ':' is spared from many places compared to Python such as annotation, 'dict' type. Because. Causer.

Module

# Module definition
module hoge
    ...
Raw
effect.md

Effect

# 'do' causer
do action(x of I8) of Effect

# Transaction
do
    Eff0
    Eff1

# 
handle
    print(cause Foo(3) + 10)
case x  # value handler
    x
case Foo(x), k  # k: continuation, x -> print(x + 10)
    k(x * x)


effect Write(str of string) of None

// write to standard ouput
def print_handler(th);
    handle:
        th():
    case x: x
    case Write(str), k:
        k(print(str))


// write to file
def write_file_handler(file, th):
    handle:
        th()
    case x: x
    case Write(str), k:
        write_file(file, str, k)


print_handler(() -> cause Write("Hello"); cause Write("World"))
# prints `Hello\nWorld`

write_file_handler("hoge.txt", () -> cause Write("Hello"); cause Write("World"))
# write "Hello" and "World" to hoge.txt

String as effect

Rationale

TODO

  • How to track effects

Reference

Raw
reference.md 
dogshow():
    dogs of -> Dog * 3 = (
        -> Dog(name = "Spot"),
        -> Dog(name = "Fido"),
        -> Dog(name = "Snoopy"),
    )
    winner of -> Dog = dogs(1)

    for dog in dogs:
        print(f"Say hello to {<- dog.name}")

    print(f"And the winner is: {<- winner.name}!")
    # All 'dogs' and 'winner' disappeared here

Existence

Raw
type.md 
# 'True'
True

# 'False'
not False

# Tautology
True(A)

# Contradiction
A(False)

# 'not' introduction
(not A)(False(A))

# 'not' elimination
False(A)(not A)

# Law of contradiction
(not A)(not A)(A)

#
B(not A)(A)

#
(not A)((B)(A) and (not B)(A))

# WARN Law of excluded middle and double negation elimination is not adopted by default
A or not A
A(not not A)

# Implication '_(_)' (operational)
B(A)

# TODO Contraposition is constructive?
(not B)(A) = (not A)(B)

# Modus ponens
B(A and B(A))

# Right association
C(B(A)) = C(B)(A)

# Peirce's law
A(A(B(A)))

# Then-1
A(B)(A)
# Then-2
(C(A)(B(A)))(C(B)(A))

# 'and' introduction
(A and B)(B)(A)

# 'and' elimination
A(A and B)
B(A and B)

# 'or' introduction
(A or B)(A)
(A or B)(B)

# 'or' elimination
(B)(A or C)(B(C))(B(A))

# Identity '=' introduction
(A = B)(B(A) and A(B)

# Identity '=' elimination
B(A)(A = B)
A(B)(A = B)

# Reflexive
A(A)

# Antisymmetric
(A = B)(B(A) and A(B))

# Transitive
C(A)(B(A) and C(B))

# Distributive
((A or C) and (B or C))(A and B or C)
((A or B) and (A or B))(A or B and C)

# Precedence 'or' < 'and' < 'not'
(not True or True) = ((not True) or True) != (not (True or True))  # 'or' < 'not'
(not False and False) = ((not False) and False) != (not (False and False))  # 'and' < 'not'

# De Morgan's laws
(not A or not B)(not (A and B))
(not A and not B)(not (A or B))

# 'all' introduction
(x of B for all x in T of Type)(A)(B(A)

# 'some' introduction
B(x of A for some x in T of Type)(B(A)

# TODO 'x' doesn't freely occur in 'A', 'B' respectively

Order

# Totally ordered
x >= y or x < y for x, y of T of Type

Probability

P(True) = 1
P(False) = 0
(P(A) <= P(B))(B(A))
P(A) + P(B) = P(A or B) + P(A and B)  # Is this meaningful?

# Conditional probability
P(B(A))
P(A) * P(B(A)) = P(A and B)  # ??

# A is independent from B
P(A) * P(B) = P(A and B)

Equivalence

Recursive type

# TODO
# recursive operation requires its name?
List = () or (T, List(T))

List = () or (T, it(T))  # Idea

Inductive type

Reduction

Intensional / extensional

Reference

Raw
x.n-tuple.md

N-tuple

A of Type, Tuple of A(I8)

(3, 5, 8)(0) = 3
(3, 5, 8)(1) = 5
(3, 5, 8)(2) = 8

(3, 5, 8)(0:2) = (3, 5)  # confusing with type annotation?
(3, 5, 8)(0..2) = (3, 5)  # or change the syntax for slice literal (0..10..2 for step?)

(3, 5, 8)(0) = 1  # should be able to assign value to function call

A of Type, D2Tuple of A(Tuple)  # or A(I8)(I8)

((0, 1), (3, 4))(0, 0) = ((0, 1), (3, 4))(0)(0) = 0
((0, 1), (3, 4))(0, 1) = ((0, 1), (3, 4))(0)(1) = 1
((0, 1), (3, 4))(1, 0) = ((0, 1), (3, 4))(1)(0) = 2
((0, 1), (3, 4))(1, 1) = ((0, 1), (3, 4))(0)(1) = 3
Raw
y.constructive.md 
# How to identify a cource?
B(A) by f

injection and surjection
mutually exclusive and collectively exhaustive
exclusive and inclusive
f of B(A)
# Monomorphism, has left (posterior) inverse: g * f = id, inner exclusive
g, h of A(C)
(g = h)(f * g = f * h)

# Epimorphism, has right (prior) inverse: f * g = id, outer inclusive
g, h of C(B)
(g = h)(g * f = h * f)

# Isomorphism, inner exclusive and outer inclusive
g of A(B)
f * g = id(B), g * f = id(A)

# Commutative: equivalence between courses
(X -> A) and (X -> B)
-> (X -> A and B) and (A and B -> A) and (A and B -> B)


# TODO How to note uniqueness?

terminal object / initial object
and / or, product / coproduct
pullback / pushout
equaliser / coequaliser

# Covariant functor
C, D of Category
F of D(C)
F(f of B(A)) = F(f) of F(B)(F(A))
F(g * f) = F(g) * F(f)
F(id_A) = id_F(A)

# Contravariant functor
F: C^op -> D
Obj(C^op) = Obj(C)
when f: D -> E at C, f: E -> D at C^op
C^op (opposite category)

# Natural transformation
C, D of Category
F, G of D(C)
θ: G(F)
(θ_C of GC(FC))_C∈Obj(C)
any f of C'(C), θ_C' * F(f) = G(f) * θ_C
θ_C (component)

# Natural isomorphism:
D^C (functor category)

sheaf preorder

adjoint and difference
morphism and relation


inner - intensive -- necessary
outer - extensive -- contingent
imply - inner inclusive?
not different because prior is small or not rich enough

Is there some duality between definition and statement?

Duality: one and another

soundness / completeness in category theory?

functional equation as external point of view of functions with category theory

isomorphic -> transformable
Raw
z.attribute.md
Raw
z.form.md

New syntax like traits in Rust and type classes in Haskell and other functionalities of various languages to replace Python's class-based object-oriented programming.

Overview

Forms

Say[T]:
    def say(self) -> str: ...


def say(t: Say) -> str:
    return t.say()


Person = Say[Person]:
    def say(self) -> str:
        return f"Hi, I'm {self.name}"

PEP 542

Dot Notation Assignment In Function Header https://www.python.org/dev/peps/pep-0542/

# You can assign to class attribute while defining function
class MyClass:
    ...


def MyClass.my_function(self):
    ...


# Or to instance attribute
my_instance = MyClass()


def my_instance.my_function(self):
    ...

Theory

Type system

Polymorphism

Nominal and structural typing

Static and dynamic dispatch

Comparison

Abstract base classes in Python

https://docs.python.org/3/library/abc.html

Traits in Rust

https://doc.rust-lang.org/beta/rust-by-example/trait.html

Type classes in Haskell

https://www.haskell.org/tutorial/classes.html

Scala

Modules in Ruby

Derivation

Meta classes in Python

Dataclass

Related topics

Duck typing

https://en.m.wikipedia.org/wiki/Duck_typing

Monkey patching

https://en.m.wikipedia.org/wiki/Monkey_patch

Mocking

https://en.m.wikipedia.org/wiki/Mock_object

Philosophy

Raw
z.operation.md

Process

What is monad?

Control

  • break
  • continue

Control operators

Order

Counting

or and and

Op0 or Op1
Op0 and Op1

Composition

Can we represent inheritance by composition?

class C(D):
    def __init__(self, x: int):
        self.x = x
    ...

class C * D(x: int):
    ...

Context

What is return?

Scope

Continuation

def before(f)(g)(x):
    return f(g(x))


def after(f)(g)(x):
    return g(f(x))


def continuation(f)(x)(g):
    return g(f(x))

Connection

Structure

operation / object

Higher-order

# PROPOSAL Curring definition
def myoperation(a: T0)(b: T1):
    pass
# constant (or nullary) is of recursively defined type
A = () -> A
C: A
C() == C  # can even sementically identical if no side effects or implicit input/output

# Fixed-point combinator
C(x) == x

zero (no) argument function

Example:

class C:
    def __init__(self, value):
        self.value = value
    def __call__(self):
        return self

So what is value? Relationship between object and value. Mutable object as an operational type.

Recursion

Complexity

Self-reference

Mode and statement

Statement changes system's operating mode.

Semantics

Temporality

Open / closed

Note

Why not function or procedure?

Philosophy

Reference

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment