caotic123

#include <stdlib.h>
#include <stdio.h>
#include <string.h>

//selection sort
#define xsort_vec(x__, t_, n, f_, p) {\
  int n_ = n - 1;\
  int i_ = 0;\
  int y__ = 0;\
  t_ t__;\

caotic123

#include <iostream>
#include <algorithm> 
#include <tuple>
#include <vector>
#include <functional>

    template <typename T>
    std::vector<T> qsort_(std::vector<T> vector,
                          std::function<bool(T i, T x)> c_m) {
  std::function<std::tuple<int, int, std::vector<T>, T> (

caotic123

However Grr don't support lambda operator is possible make a fixed point using just replacement string(like the language was constructed).

[Ώ <- s(i)(i)(e(p(s(i)(i)))) : JUST A FIXED POINT 
u(f) <- f(s)(k) : IOTA COMBINATOR
d <- k(i) catch 2 vaues ignore the first and return the second
s(x)(y)(z) <- x(z)(y(z))
k(x)(y) <- x
i(x) <- s(k)(k)(x)
e <- s(k)(k(s(i)))
]

caotic123

Abstraction type system

Type system is a construction for guarantees safely in a language, though exist many other aplications like metaprogramming... It's means that i can writes a program but with a safe way, sure it's is perfect why it's solve many problems that programmers has after of compilation. The main idea that i can encode and represent a subset of solutions with a safe type system and better maybe the type can help me represent that.

Data representing

Ok it's mean i have a safe type system and i could represent my types of data..... Ok sure...., but no... limited type system have a weak power of abstraction(no i am not talking about c++ but yes a little part of the language).

The problem of "pair"

Let's go represent a pair: Pair is a tuple of the two values like (P x y), where x and y are values, in this discussion the values x and y can be encode a T type and a Tuple T type.

caotic123

Despite simply typed lambda calculus is total(and it means that is not Turing complete why it's strongly normalizing and ever halts) can represent data(church encoding). Simply typed lambda calculus is not Turing completeness, but expressive.

We let's consider this:

n x f = f x
k f x a = f (a x) a

Where let d = k(k (k (n))) (0) (\x -> x+1), IO::print(d) will print d evalued as 4. Then...k will count until n function.

caotic123

Before everything Kei name isn't a official, but can to be (i don't know yet), therefore i will accept suggestions. The idea of kei is for creating safe mini-libs for system language programming like c++ with a high level of predictability of compilation with small specifics functional optimizations. Let's go to rules of typed lambda calculus:

x : σ E T,            x is a constant type of T',             T, x:σ |- e:t                       T |- n : σ -> t T |- k : σ 
T |- x : σ            T |- c:T'                               T |- (λx:σ. e):(σ -> t)             T |- (n k):t

Fine, now let's go to introduce kei language: Give a function that receives T and returns T:

caotic123

import Control.Monad
import Data.Maybe
import qualified Data.Set as Set
import qualified Data.Map.Strict as Map

data Puzzle = Puzzle [Int] Int Int Int deriving Show

heuristic_comp :: [Int] -> Int
heuristic_comp [] = 8
heuristic_comp (x : xs) = do 

caotic123

∇R←IDENTITY N
  R←(N N)⍴(1,N⍴0)
∇

∇R←EXTENDBOTTOM MAT
  R←(((↑⍴MAT)⍴1),0)\[1]MAT
∇

∇R←EXTENDRIGHT MAT
  R←(((2⌷⍴MAT)⍴1),0)\MAT

caotic123

import java.net.*;
import java.io.*;
import java.util.LinkedList;
import java.util.Queue;
import java.util.concurrent.Callable;
import java.util.concurrent.ExecutorService;
import java.util.concurrent.Executors;
import java.util.concurrent.Future;
import java.util.function.*;

caotic123

In Agda : 
{-# OPTIONS --with-K #-} -- This is optional just be aware that overrides the option --without-K

data _≡_ {w : Set} (_x : w) : w -> Set where
  refl : _x ≡ _x

axiom_k : ∀ {A : Set} {a : A} (P : ∀ (H : a ≡ a) -> Set) (H : P refl) (E : a ≡ a) -> (P E)
axiom_k p H refl = H

In Kei :