Nethra - Proof of concept for a minimal core language based on dependant function type and dependant pair

Overview

Nethra

Terms

n in Ident
i in Int
c in Char

e ::=
    Type_i                -- Type at level i
    n                     -- Variable
    
    data(n:e)             -- Constructor ???
    i                     -- Integer literal
    c                     -- Character literal
    
    Π(n:e).e   Π{n:e}.e   -- Dependant function type
    λ(n).e     λ{n}.e     -- Function
    e e        e {e}      -- Application
    
    Σ(n:e).e              -- Dependant pair type
    e , e                 -- Pair
    fst e                 -- Left projection
    snd e                 -- Right Projection
    
    e + e                 -- Disjunction
    inl e                 -- Left injection
    inr e                 -- Right injection
    case e e e            -- Catamorphism
    
    μ(n).e                -- Recursion
    fold (μ(n).e) e       -- Fold recursive type
    unfold (μ(n).e) e     -- Unfold recursive type
    
    e ∈ e                 -- Term inhabits Type
    
    ?n                    -- Hole for inference

Typing rules

Hierarchy and hypothesis

---------------------     ----------------
Γ ⊢ Type_i : Type_i+1     Γ, x : T ⊢ x : T

Literals and constructors

l ∈ int         l ∈ char
-----------     ------------     -----------------
Γ ⊢ l : int     Γ ⊢ l : char     Γ ⊢ data(n:T) : T

Dependant function type

Γ, x : M ⊢ N : T
----------------
Γ ⊢ Π(x:M).N : T

Γ, x : A ⊢ B : T          Γ, x : A ⊢ B : T
---------------------     ---------------------
Γ ⊢ λ(x).B : Π(x:A).T     Γ ⊢ λ{x}.B : Π{x:A}.T

Γ ⊢ f : Π(x:M).N   Γ ⊢ e : M      Γ ⊢ f : Π{x:M}.N   Γ ⊢ e : M 
----------------------------      ----------------------------
Γ ⊢ f e : N[x=e]                  Γ ⊢ f {e} : N[x=e]            

Γ ⊢ f : Π{x:M}.N   Γ, v:M ⊢ f {v} e : N
---------------------------------------
Γ ⊢ f e : N

Dependant pair type

Γ,x : A ⊢ B : T
----------------
Γ ⊢ Σ(x:A).B : T

Γ ⊢ A : M   Γ ⊢ B : N[x=A]
--------------------------
Γ ⊢ A,B : Σ(x:M).N

Γ ⊢ p : Σ(x:M).N
----------------
Γ ⊢ fst p : M

Γ ⊢ p : Σ(x:M).N
----------------------
Γ ⊢ snd p : N[x=fst p]

Disjunction

Γ ⊢ A : T   Γ ⊢ B : T
---------------------
Γ ⊢ A + B : T

Γ ⊢ A : M
-----------------
Γ ⊢ inl A : M + N

Γ ⊢ A : N
-----------------
Γ ⊢ inr A : M + N

Γ ⊢ a : A + B   Γ ⊢ l : A -> C   Γ ⊢ r : B -> C
-----------------------------------------------
Γ ⊢ case a l r : C

Recursion

Γ, x : T ⊢ A : T
----------------
Γ ⊢ μ(x).A : T

Γ ⊢ A : N[x=μ(x).N]
---------------------------
Γ ⊢ fold(μ(x).N) A : μ(x).N

Γ ⊢ A : μ(x).N
----------------------------------
Γ ⊢ unfold(μ(x).N) A : N[x=μ(x).N]

Term inhabitation

Γ ⊢ x : T
---------------
Γ ⊢ (x ∈ T) : T
You might also like...
The sample App implements type safe SQL by JOOQ & DB version control by Flyway

The sample App implements type safe SQL by JOOQ & DB version control by Flyway Setup DB(PostgreSQL) $ docker compose up -d Migration $ ./gradlew flywa

Bring type-safety to your GitHub actions' API!
Bring type-safety to your GitHub actions' API!

GitHub Actions typing Bring type-safety to your GitHub actions' API! This is a GitHub action that validates your action's type specs (action-types.y(a

The WeeBe application is a social media-type app built on Ktor framework

The WeeBe application is a social media-type app built on Ktor framework that allows users to exchange various content connected with mental health, motivation, psychology, and improving oneself. Users can share posts with texts, images, videos, and links, as well as discuss the content in the comment section

It is a project that contains lessons and examples about Kotlin programming language. 🇰
It is a project that contains lessons and examples about Kotlin programming language. 🇰

Kotlin Tutorials What is Kotlin? I added the platforms it supports and great resources. You can access the article from the link below: https://medium

Android Multi Theme Switch Library ,use  kotlin language ,coroutine ,and so on ...
Android Multi Theme Switch Library ,use kotlin language ,coroutine ,and so on ...

Magic Mistletoe Android多主题(换肤)切换框架 背景 时隔四年,在网易换肤之前的思路下,做了几点改进,现在完全通过反射创建View,并且在SkinLoadManager中提供一个configCustomAttrs以支持自定义View的属性插队替换 摈弃了之前的AsyncTask

Kotrlin Programming Language Cross-Platform Development which includes Android, iOS and Backend. Pretty much everwhere.
Kotrlin Programming Language Cross-Platform Development which includes Android, iOS and Backend. Pretty much everwhere.

Kotlin-Everywhere: Kotlin Programming Language Cross-Platform Development This is still a WIP but the idea is to create a tiny KOTLIN project that cou

The Okila server project uses the Spring boot framework and uses the Kotlin language

Okila-Server The Okila server project uses the Spring boot framework and uses the Kotlin language Format Response //The response successfully format

Demonstration of Object Pool Design Pattern using Kotlin language and Coroutine
Demonstration of Object Pool Design Pattern using Kotlin language and Coroutine

Object Pool Design Pattern with Kotlin Demonstration of Thread Safe Object Pool Design Pattern using Kotlin language and Coroutine. Abstract The objec

Owner
Lambë Language
Lambë language ecosystem
Lambë Language
Muhammad Valian Masdani 2 Jul 5, 2022
A scalable cluster computing proof-of-concept that calculates prime numbers upto 2^32!

Project Crumbler An proof-of-concept of oppurtunistic computing which also uses cluster computing This serves as a project as part of the Cloud Comput

Hemanth Krishna 3 Feb 18, 2022
Kotlin extension function provides a facility to "add" methods to class without inheriting a class or using any type of design pattern

What is Kotlin Extension Function ? Kotlin extension function provides a facility to "add" methods to class without inheriting a class or using any ty

mohsen 21 Dec 3, 2022
FizzBuzzKotlin - A function fizzBuzz to generate a list of string based on the input number

FizzBuzzKotlin write a function fizzBuzz to generate a list of string based on t

gson 0 Feb 12, 2022
An Interpreter/Transpiler for the Folders esoteric programming language, a language with no code and just folders

Folders2kt ?? An Interpreter/Transpiler of the Folders esoteric programming language, a language with no code and just folders, written in Kotlin Show

Jens Klingenberg 18 Jan 4, 2023
A custom view for rating which easy to make and use, but function is excellent

QRatingView A custom view for rating which easy to make and use, but function is excellent Effect Picture Properties <declare-styleable name="QRat

QCoder 1 Dec 3, 2021
Automatically generates UI demos which allow users to call any function with any parameters

Automatically generates UI demos which allow users to call any function (including composable ones) with any parameters. Useful for building demo screens in playground apps of various design systems.

Anton Popov 3 Jul 28, 2022
FragmentContainerViewIdBugDemo - minimal repro project demonstrating a bug in FragmentContainerView's id check logic in the context of a dynamic feature module

FragmentContainerViewIdBugDemo minimal reproduce project demonstrating an apparent bug in FragmentContainerView's id check logic in the context of a d

null 0 Jan 5, 2022
Firestore Kotlin Client with strict (and relaxed) type-system.

Firestore Kotlin Client with strict (and relaxed) type-system.

Vihang Patil 2 Mar 4, 2022
Esito ambition is to be your return type for suspending functions.

Esito ambition is to be your return type for suspending functions.

null 58 Oct 21, 2022