pedrominicz

module Combinator where

-- https://crypto.stanford.edu/~blynn/lambda/sk.html
-- http://okmij.org/ftp/tagless-final/ski.pdf
-- https://www.cantab.net/users/antoni.diller/brackets/intro.html

import Data.List

type Name = String

pedrominicz

module Lambda where

-- https://www.youtube.com/watch?v=O0TgP7GKkSY
-- https://gist.github.com/pedrominicz/127ab01cec689cc3d69f32e6c4f758bb

data Term
  = App Term Term
  | Lam Term
  | Var Int
  deriving (Eq, Show)

pedrominicz

module Tactic where

import Data.List

-- https://totbwf.github.io/posts/tactic-haskell.html

data Type
  = Var Int
  | Arrow Type Type
  | Prod Type Type

pedrominicz

{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Early where

-- https://chrisdone.com/posts/exceptt-vs-early-do/
-- https://hackage.haskell.org/package/unliftio-core-0.2.0.1/docs/src/Control.Monad.IO.Unlift.html#MonadUnliftIO
-- https://hackage.haskell.org/package/unliftio-0.2.14/docs/src/UnliftIO.Internals.Async.html#concurrently

pedrominicz

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TupleSections #-}

module Optic where

-- https://twanvl.nl/blog/haskell/cps-functional-references
-- https://mail.haskell.org/pipermail/haskell-cafe/2007-November/035263.html

import Control.Applicative
import qualified Control.Category as Cat

pedrominicz

module Optic where

import Prelude hiding (fst, (.))
import qualified Prelude

-- https://twanvl.nl/blog/haskell/overloading-functional-references

data FRef s a = FRef
  { get :: s -> a
  , set :: a -> s -> s

pedrominicz

{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Main where

pedrominicz

{
module Lazy where

import Data.Foldable
import qualified Data.ByteString.Lazy as B
}

%wrapper "basic-bytestring"

$alpha = [a-zA-Z]

pedrominicz

import tactic

-- https://www.youtube.com/watch?v=l1FCXUi6Vlw

namespace yoneda

class functor (f : Type → Type) : Type 1 :=
(map : ∀ {α β : Type}, (α → β) → f α → f β)
(id_map : ∀ {α : Type}, map (id : α → α) = id)
(comp_map : ∀ {α β γ : Type} (g : α → β) (h : β → γ), map h ∘ map g = map (h ∘ g))

pedrominicz

#!/usr/bin/env python3

import bs4
import sys

if len(sys.argv) != 3:
    print(f'usage: {sys.argv[0]} <tag> <file>')
    sys.exit(1)

with open(sys.argv[2], 'r+') as f: