Treesolang

Treesolang (better name pending) is a fusion between esolangs like Thue and Fuun DNA and the lambda calculus, and is therefore a 'declarative, functional, string-replacement language', I guess. It was created by Baidicoot in early 2019 as a way to standardize the description of axiomatic logical systems like the Peano axioms, and was inspired by the Haskell type system.

Implementation here. (NOTE: requires GHC to compile)

Program Structure

Each Treesolang program consists of many of two types of top-level expression: declarations and rules. First, declarations. A declaration comes in the form:

data <Name> :: <Type>

where 'Name' is a capitalised identifier, and 'Type' is an arity expression. Arity expressions in turn consist of:

<arity> -> <arity> | <variable> | *

where 'variable' is a lowercase string. The '->' refers to a function type like in the simply typed lambda calculus and is an operator between two arities, while '*' is the 'base' type (note that this is useless, but exists for historical reasons). For example, the 'Succ' (successor operator) could be defined like so:

data Succ :: * -> *

i.e. it takes a base type and returns a base type. A declaration can also be infix (i.e. the operator comes after its first operand), as long as the 'Name' only consists of special characters:

infix . :: (b -> c) -> (a -> b) -> a -> c

The other top-level expression, a rule, comes in the form:

~ <pattern> => <result>

where 'pattern' and 'result' are both lists of operator application like in combinatory logic, with parenthesies, but with pattern matching like in Haskell. The resulting arity of 'pattern' and 'result' must match. These restrictions ensure that arity can be done away with at runtime.

Program Execution

The execution method for Treesolang involves the repeated application of matching 'patterns' (rules) and the replacement of those matched patterns with their corresponding 'results', in the order that they were defined in the program. As a string replacement language, execution is nondetermanistic, and so patterns are always applied as soon as possible. Each program starts with the string of the single operator 'Main :: x':

~ Main => Your Code (Goes here)

Examples & Turing-Completeness

Treesolang is trivially turing-complete, as one can easily encode combinatory logic into it:

data S :: (a -> b -> c) -> (a -> b) -> a -> c
data K :: a -> b -> a
data I :: a -> a

~ I x => x
~ K x y => x
~ S x y z => x z (y z)

For extra funlolz here's the Peano numerals under addition:

data Zero :: *
data Succ :: * -> *
infix + :: * -> * -> *

~ x + Zero => x
~ (Succ x) + n => Succ (x + n)

I/O

I/O is achieved in Treesolang with the 'PutChar :: * -> *' operator which prints out an ASCII character with a value equal to the data structure depth of the value fed into it (e.g. evaluates a peano numeral to an integer). The 'PutStr :: * -> *' takes a linked list of characters and prints that. Both these I/O actions evaluate their inputs fully beforehand, and output an 'IO :: *' action that when applied with a 'DoIO :: * -> *' operator does the IO action.

Input is handled by a 'GetChar :: *' operator which, when evaluated, outputs a peano numeral with value equal to the top item on the input buffer.

Challenges

1. Make a Quine