kritzcreek

[package]
name = "cont-rs"
version = "0.1.0"
authors = ["kRITZCREEK <christoph.hegemann1337@gmail.com>"]
edition = "2018"

# See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html

[dependencies]
sexp = "1"

Nikolaj-K

In this video we come across about 50 online resources for category theory:

https://youtu.be/hEW42ARKNoE

I quickly comment on about 20 major ones. I link to the university sites, arXiv sites or Amazon page - most of the mentioned books are online available.

Here's another category theory list on github

https://github.com/prathyvsh/category-theory-resources

cheery

-- The linear abstract machine
-- as described in the "The Linear Abstract Machine"

-- Environment is a representation of a canonical combinator
-- the canonical combinator u ⊗ v is represented by Ja, and 1 by Nil
-- the canonical combinator y ∘ v represented by Comb: y is piece of code.
--
-- Code is list of primitive instructions.
--
-- Sequential composition becomes concatenation (in opposite order),

i-am-tom

{-# LANGUAGE DataKinds               #-}
{-# LANGUAGE PolyKinds               #-}
{-# LANGUAGE TypeOperators           #-}
{-# LANGUAGE UndecidableInstances    #-}
{-# LANGUAGE UnsaturatedTypeFamilies #-}

import GHC.TypeLits
import Prelude hiding (Functor, Semigroup)

type Main = (Fizz <> Buzz) <$> (0 `To` 100)

iitalics

#lang racket/base
(require
 racket/string
 racket/port
 racket/system
 racket/match
 racket/format)

(module+ test
  (require

ChristopherKing42

--Roughly based on https://github.com/Gabriel439/Haskell-Morte-Library/blob/master/src/Morte/Core.hs by Gabriel Gonzalez et al.

data Expr = Star | Box | Var Int | Lam Int Expr Expr | Pi Int Expr Expr | App Expr Expr deriving (Show, Eq)

subst v e (Var v')       | v == v' = e
subst v e (Lam v' ta b ) | v == v' = Lam v' (subst v e ta)            b
subst v e (Lam v' ta b )           = Lam v' (subst v e ta) (subst v e b )
subst v e (Pi  v' ta tb) | v == v' = Pi  v' (subst v e ta)            tb
subst v e (Pi  v' ta tb)           = Pi  v' (subst v e ta) (subst v e tb)
subst v e (App f a     )           = App    (subst v e f ) (subst v e a )

gallais

{-# LANGUAGE GADTs                #-}
{-# LANGUAGE DataKinds            #-}
{-# LANGUAGE TypeFamilies         #-}
{-# LANGUAGE RankNTypes           #-}
{-# LANGUAGE PolyKinds            #-}

module STLC where

-- Defining type and the corresponding singletons

xero

                        ..:77I777777777777777777777I. .                         
                     ..?77777777777777777777777777777$+..                       
                   . ~7777777I7777777777777777777777777$~..                     
                    .7I7777...7777777777777777777777777$7+.                     
                   .?7777..   ..77777777777777777777777$$7.                     
                   .77777       777777777777777777777$$$$$I                     
                   .77777..  ...7777777777777777777$$$$$$$$                     
                   .7777777  .77$777777777777777777$$$$$$$$                     
                   .77777777777777777777777777777$$$$$$$$$$                     
                   .77777777777777777777777777$$$$$$$$$$$$$                     

shangaslammi

s x y z = x z (y z)
k x y   = x
i       = s k k
c       = s (s (k (s (k s) k)) s) (k k)
b       = s (k s) k

hello =
    s(s(k s)(s(k k)(s(k s)(s(k(s(k s)))(s(s(k s)(s(k k)(s(k b)i)))(k(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s
    b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(c k))))))))))))))))))))))))))))))))))))))))))
    )))))))))))))))))))))))))))(s(s(k s)(s(k k)(s(k s)(s(k(s(k s)))(s(s(k s)(s(k k)(s(k b)i)))(k(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s b(s