Notes

Tinker the Kludge

work

December 14, 2022 — sameer

Work

1. Things I

1.1. work on

1.1.1. issues like

  1. space leaks with and number of calls made to writer monads
  2. slow compilation of zk-roofs
  3. rarely extend existing emacs packages for nyxt
  4. nixos-ci+git, sharing,deploying code over ssh (includes the unpaid work, IP available on request)

1.2. am working on

1.2.1. My builds for ocaml-xenstore, sbcl work on my nix-shell(s) , once I can't think of any more of such shells, I ll use them as buildinput reference for my remote-flakes

1.3. Can work on

1.3.1. give a Haskell talk, but rarely and provisionally

1.3.2. running my builds on sbc,soc, fpga

1.4. want to work on

1.4.1. Verifying if induction means well ordering with coq or idris and all the paper or posts I have found pairwise contradictory

Preparing for both

2. Don't work on

2.1. linkedin profile

2.2. Windows

2.3. OOP - esp Java

2.4. anything else I don't want to do

3. Who pays me for it:

3.1. blockchain folks

3.2. Processor dev folks

3.3. Who can pay me for it

3.3.1. verification and proof engineering folks

3.3.2. Secure Microkernel folks

3.3.3. sel4 and also freeRTOS, mBed, Genode,

3.4. system programmers

3.4.1. unikernels

3.4.2. Haskell/ FP consulting folks

3.5. DB folks

3.5.1. xen hypervisor and irmin

3.6. Who doesn't pay me for it

3.6.1. fast track projects - quick and dirty deliverable

4. work experience

4.1. available on request

5. Education

5.1. Dropout

5.1.1. UG iitb [2006-]

5.2. work experience available on request

6. Contact

6.1. xameer @mathstodon

<p>Tags: GHC, Lisp, Ocaml, Type Theory, Tech Stack</p>

Author: System administrator

Created: 2022-12-14 Wed 19:13

Validate

Comments?  

Types and impredicativity

November 06, 2022 — sameer

Decidability

why it matters?

Because your program can have more bits than there are atoms in universe.

Also when reduction doesn't normalize the expresssion

Function types in haskell for inststance aren't decidable, with due exceptions. Analogy

Logic TT Haskell
P A a
P/\Q A*B (a,b)
P->Q A->B either(a,b)
∀ x P(x) ∏ a: a P(a)  
∃ x P(a) ∑ a: a P(a)  
proof inhabitant program

Progamming construct as corresponding (ir of ) logic

logic construct
linear rust borrow checker , cbpv
double negation, classical csp, cbpv
mu calculus call cc
system f stlc + parametric polymorphism
modus ponens eval map
material implication, currying adjunction exponential object
tautology terminal object has a global preposition
modality provability in axiom-K
modus ponens : resolution substitution,subtyping, function application
ch, aoc imcrecdicative
skolem, unification, sequent tebleaux prolog
modal logic referential transparency
modal algebra boolean algebra + unary op
prepositional invariant in bisimulation
fol no normal forms
terms:lamda calc to combinatory logic ch-deduction meta theorem
   

Type theory and Poperties

tt Property
mltt everything terminates

Questions

constuctivity is needed for computability , would you say that about predicativity ?

It turns out if you tweak ZF in the right way, and remove EM, you get a perfectly fine constructive logic, i.e. a theory in which every function nat -> nat can be realized by some lambda term.

Harder to say what happens at other function spaces though… tweet

blog.jpg

table 1 reference

Papers

intuitionistic games : determinacy , completeness and normalization

automata theory approach to inutionistic logic

objects of interest

Axiom K

constructive

intutionistic

logicians

Fitch

Simpson

Shelah 1

Prawitz 2

Vitali 3

Induction

bar induction

l¨ob induction 🏿

Footnotes:

1

zf without hamel basis, \L2 [0,1]

2

ND forintutionistic modal

3

consistency of inaccessible cardinals

Author: System administrator

Created: 2022-11-16 Wed 11:18

Validate

Comments?  

November 01, 2022

Comments?  

Org as a db?

October 29, 2022 — sameer

In everyday life

Versioning these blog posts with org-roam and not git

I insert one org-roam noade for every new blog-post I –rarely write and often update– here and quite often I want to know how did I end up with the current version of the post.

Find that node with org-roam to edit it, instead of default drafts

edit, save , exit , now I have both versions in my-graph.

To publish I ll just ./bb.sh edit $PostName , find the node1 and expost the latest PostNamedotorg as html and replace that with html of existing post , save, exit scp.

risks of evolution

you can use properties drawer to implement simple database capabilities, but it has one important limitation - values are mere text, so you can’t have real Org mode links there, meaning that Element API, Org roam and some other tools do not recognise them as links.

agenda on top of the cached data? , to instead expose an API to build the interface from a different data source

will org-roam’s caching model work at larger scales? rgrep isn’t magic, it’s literally just grep -r or recursive grep, something that all *NIX users are familiar with

org-roam’s functions are just a read-only interface on top of the database layer. how can users specify their own schema, when the schema and how the database is populated is very much tied to what’s being pulled out of each Org file?

should org-roam provide a core for managing metadata (including links) with APIs to build on top of that (like org-roam-buffer, dailies, agenda and other stuff) which could be shared either in the org-roam repository or separately.

Footnotes:

1

Unlike node name, the name of the file will change after every edit, but thats no trouble , as org-roam searches by node name and not by file name

Author: System administrator

Created: 2022-11-16 Wed 10:26

Validate

Comments?  

October 29, 2022

Comments?  

Refactoring in Nixos

October 24, 2022 — sameer

Why

CI/CD without continuous refactoring is digital equivalent of horading – @GrdayBooch

Test case - Lisp env for Emacs

What

You are doing n projects with conflicting deps,envs and due overlaps.

Intersection I in configuration.nix.

In shell.nix

  • override the conflicting part of I - mkderivation
  • inherit the needed part of I - mkshell
  • declare the remainder
  • pin versions with niv or git-commits

Instead of too many crossing symlinks

This gets tricky

Say you get sbcl in a ~/workdir with nix shell, which doesn't import system env

How

Say your make file for a lib/package has both internal and of course external conf

mySourceRegexes = [
   "^app.*$"
   "^.*\\.cabal$"
   "package.yaml"
 ];

Deps

Self

Itself - (recursive) 1

Super

Let application or function to Compose everything else and return to self, add set of all the properties, itself, constraints , accessed dep paths to it, as your function composes everything (dep from self and returns everything to itself. Its like symlinking or man fetching clothes fromt the closet and wearing them.

Loops in, loops around

the sub/supersets of parametrs , as it accesses them and fetches them

What does it call itself

attr

Trasitive dep 2

code can generate them and parse them, like a graph

name

pname

shell name

env name

Transitive closure of dependency relationships - Includsion of references

You can define the process precisely with Natural Deduction using the inference rules

how do they combine ?

Like sur/nick name

attrname + commit hash -> version

pname3 $INPUT, version -> package name

curl -/-> any of this : pure vs impure

How does it call itself

callpkg

let

otherwise

Key ideas

system is not a package and vice versa

However, a package p may depend d on other set of system-level-packages s : {S} or its own set of plugins packages q: {Q}

This can be resolved by either

symlinking the store derivation path to the package dir of src

writing a pill to build p and calling s,q from it to get p'

writitng a flake with builinputs including q,s, get p''

pinning to the git commit of p, eg using import ,which has q,s' in the system level flake or config file

write a shell which does one or more of the above to keep the p-env independent of system level env

more provisioning , refactoring

Observations

in/correct builds can share the profile, so profile is innocent, unless found otherwise.

Analysing the diff of the build (or profile) pair can help trace the exact culprit, do that before filing a bug report

flake –rollback or switch-generation works, iff you have an older profile, else you need to reboot from the last working profile and then rebuild-switch be get the configuration, building which you broker the build/

Once fixed set that profile as default boot

deterministic

later

Process Isolation

one process/ kernel/machine/ metal , unlike flakes , to which you can add as many build inputs as you need.

OS Kernel machine Metal
  sunixi Metal  
  hermitux docker Pine
Nixos Genode    
  OSv firecracker RISC V
       

Logic in Flakes

patterns

single repository

Gentoo puts package descriptions all in a single repository.

"inputs" pattern allows our expressions to be easily customizable through a set of arguments. These arguments could be flags, derivations, or whatever else. Our package expressions are functions

reaptedly overriding , reusing patterns and keeping them maintainable

using a central repository like nixpkgs, and defining overrides on our local machine without even modifying the original package

Footnotes:

1

prefer super over rec, composition over recusrion.

2

c.f. check ghc rules regarding transitive dep

3

Not all derivations use pname

Author: System administrator

Created: 2022-11-16 Wed 10:01

Validate

Comments?  

October 23, 2022

Comments?  

Topology and set theory

October 22, 2022 — sameer

set theories I ve visited

stratified lambda calculus

Think about it

evaluation by reduction ie substituion - integration

confluence is related to convergence

It's somewhat fair to call it calulus, depending on how you see calculus

Bishop's

Russel's

HoTT and Topos

⊥ :≡ 0

T :≡ 1

P ∧ Q :≡ P ∗ Q

P ∨ Q :≡ || P + Q ||

P ⇒ Q :≡ P → Q

∀ (x : A) ⋅ P(x) :≡ ∏ (x:A) ⋅ P(x)

∃ (x : A) ⋅ P(x) :≡ || ∑ (x :A) . P(x) ||

Chesterton

a small circle is quite as infinite as a large circle

cauchy sequences does not have same topology as \R , it has topology of cantor space.

every cauchy real has a dedekind cut

why stop at that

A map f: house -> city between topological spaces is said to be continuous if, for every open set U ∈ (house) , f-1(city) is open in house. 1

Objects of interest

zfc with grothendieck universes - resizing principles, lem, simplical set, fpqc

Question

can sets alone index sets?

Theorems of interest

Banach alaouglu

Banach fixed point

paradoxes

banach tasrki

cantor

Russel

Martin

liar's

Point free Topology

Bye AOC! Hello Constructivism.

    to/as coq
reifier point free pointed  
  type declaration functor  
  infix compose curried function ::
  unix script sum = foldr (+) 0  
  concatenative land eval over different categories  
       

Footnotes:

1

that's right, I just described ε δ definition of limit there.

Author: System administrator

Created: 2022-11-01 Tue 16:08

Validate

Comments?