Spartan implementation of H.O.T.T.

Overview

Down The Path

I was walking down the line,
Trying to find some peace of mind.
Then I saw you,
You were takin' it slow,
And walkin' it one step at a time.

A spartan implementation of H.O.T.T.

Quick Examples

"If you're lost now,
Maybe I could help you along and sing you a song,
And move you on."

I haven't implemented parsers for whole files yet. But I can already parse and print individual terms.

Ordinary MLTT stuff:

λ (t : U) (x : t) => x
Π (t : U) (x : t) => t

Dependent pairs are annotated the type of the second component with a peculiar syntax.

λ (t : U) (x : t) => t { t' => t' } x
Π (t : U) (x : t) Σ (t' : U) => t'

fst and snd are prefixes that have the highest priority, so f fst snd p q stands for (f(fst(snd(p))))(q):

λ (T : U) (S : Π (_ : T) => U) (p : Σ (t : T) => S t) => snd p
Π (T : U) (S : Π (_ : T) => U) (p : Σ (t : T) => S t) => S fst p

ap and Id without dependency:

ap[ . y]
Id[ . A][y, y]

When we deal with n-ary ap and Id, we need to explicitly mark the LHS and RHS of the equations:

ap[z / ap[ . x] : x == x . y]
Id[z / ap[ . x] : x == x . A][y, y]

And of course this one reduces to the one above it.

Type Theory

She said
"I'm looking for a kind of shelter,
No place for me to call my own.
I've been walking all night long, but
I don't know where to call my home."

  • Start out with 0,1,∑,∏,U. (2, Nat are slightly more complicated.)
  • Get to the meat.
    • Typechecking rules for HOTT primitives, which I think should be ap, Id, sym, , .
    • Reduction rules for all those. For simple reduction rules, we should introduce 6 more primitives, which all individially behave well. But that impedes type checking.
  • Inductive types.
  • Higher inductive types.
  • Inductive families.

For inductive types (even 2), we need to make Id, ap stuck on neutral terms. So for instance Id[. A+B][inl a, inl b] would compute to Id[.A][a,b], just as the HoTT book describes. Alternatively we can just make Id compute into a case analysis. Not sure which would be easier.

We might be able to come up with syntactic restrictions on HITs to make it work.

The code files have some comments at the top where you can read a little more about my thoughts.

Implementation

"The only way to find that place is
Close to where my heart is.
I know I'm gonna get there,
But I've got to keep on walking down the line."

Python has got a couple of cool features like assignment expressions and structural pattern matching. I'm trying to write python code in a semi-pure style.

Down the line

I said
"You go on walking down the line,
Wasting all your precious time.
But you're never gonna find it,
Because there is no end to the line,
There's no destination for to find."

(...)

Owner
Trebor Huang
I'm an undergrad at Tsinghua University. / I like mathematics and dependent type theory.
Trebor Huang
Sublime Text 2/3 style auto completion for ST4

Hippie Autocompletion Sublime Text 2/3 style auto completion for ST4: cycle through words, do not show popup. Simply hit Tab to insert completion, hit

Alexander Schepanovski 20 May 19, 2022
Santa's kitchen helper for python

Santa's Kitchen Helper Introduction/Overview Contents UX User Stories Design Wireframes Color Scheme Typography Imagery Features Exisiting Features Fe

Paul Browne 4 May 31, 2022
Modern robots.txt Parser for Python

Robots Exclusion Protocol Parser for Python Robots.txt parsing in Python. Goals Fetching -- helper utilities for fetching and parsing robots.txts, inc

Moz 176 Dec 16, 2022
This tool for beginner and help those people they gather information about Email Header Analysis, Instagram Information, Instagram Username Check, Ip Information, Phone Number Information, Port Scan

This tool for beginner and help those people they gather information about Email Header Analysis, Instagram Information, Instagram Username Check, Ip Information, Phone Number Information, Port Scan.

cb-kali 5 Feb 18, 2022
addon for blender to import mocap data from tools like easymocap, frankmocap and Vibe

b3d_mocap_import addon for blender to import mocap data from tools like easymocap, frankmocap and Vibe ==================VIBE================== To use

Carlos Barreto 97 Dec 07, 2022
Create standalone, installable R Shiny apps using Electron

Create standalone, installable R Shiny apps using Electron

Chase Clark 5 Dec 24, 2021
Explores the python bytecode, provides some tools to access it for fun and profit.

Pyasmtools - looking at the python bytecode for fun and profit. The pyasmtools library is made up of two parts A python bytecode disassembler . See Py

Michael Moser 299 Jan 04, 2023
Addons like multipages for streamlit webapp

streamlit_pages Installation $ pip install streamlit-pages Features Adding multiple pages to streamlit Sharing specific pages Usage import streamlit

36 Dec 25, 2022
Superset custom path for python

It is a common requirement to have superset running under a base url, (https://mydomain.at/analytics/ instead of https://mydomain.at/). I created the

9 Dec 14, 2022
Have an idea for a Python package? Register the name on PyPI 💡

Register Package Names on PyPI Have an idea for a Python package? Thought of a great name? Register it on PyPI, before someone else does! A tool that

Alex Ioannides 1 Jul 15, 2022
A faster Python generator that get function results from multi-process workers

multiyield This package implements a Python generator that get function results from multi-process workers. The faster_fifo Queue (instead of the stan

Xin Du 1 Nov 18, 2021
A tool to help calculate how to split conveyors in Satisfactory into specific ratios.

Satisfactory Splitter Calculator A tool to help calculate how to split conveyors in Satisfactory into specific ratios. Dependencies Python 3.9 PyYAML

RobotiCat 5 Dec 22, 2022
Expense Tracker is a very good tool to keep track of your expenseditures and the total money you saved.

Expense Tracker is a very good tool to keep track of your expenseditures and the total money you saved.

Shreejan Dolai 9 Dec 31, 2022
My collection of mini-projects in various languages

Mini-Projects My collection of mini-projects in various languages About: This repository consists of a number of small projects. Most of these "mini-p

Siddhant Attavar 1 Jul 11, 2022
Zeus - Advanced Punishments with Embeds.

Zeus Advanced Punishments with Embeds. Make sure to put the Discord Bot Token in the " TOKEN = '' " Language Python Features Ban Kick Mute Unmute Warn

2 Jan 05, 2022
8 Nov 04, 2022
PSP (Python Starter Package) is meant for those who want to start coding in python but are new to the coding scene.

Python Starter Package PSP (Python Starter Package) is meant for those who want to start coding in python, but are new to the coding scene. We include

Giter/ 1 Nov 20, 2021
OntoSeer is a tool to help users build better quality ontologies

Ontoseer This document provides documentation for the first version of OntoSeer.OntoSeer is a tool that monitors the ontology development process andp

Knowledgeable Computing and Reasoning Lab 9 Aug 15, 2022
SpellingBeeSolver - This program generates solutions to NYT style spelling bee problems.

SpellingBeeSolver This program generates solutions to NYT style spelling bee problems. The initial version of this program is being written in Python

1 Jan 01, 2022
Collections of python projects

nppy, mostly contains projects written in Python. Some projects are very simple while some are a bit lenghty and difficult(for beginners) Requirements

ghanteyyy 75 Dec 20, 2022