oisdk

import GHC.Base (build)
import Data.Function (fix)

unfoldl :: (b -> Maybe (a, b)) -> b -> [a]
unfoldl f b = build (\c nl -> fix (\r a -> maybe a (uncurry (r . (`c` a))) . f) nl b)

oisdk

import GHC.Base (build)

-- | Groups adjacent elements according to some relation.
-- The relation can be an equivalence:
--
-- >>> groupBy (==) "aaabcccdda"
-- ["aaa","b","ccc","dd","a"]
--
-- >>> groupBy (==) []
-- []

oisdk

{-# LANGUAGE ViewPatterns, PatternSynonyms #-}

import Control.Arrow
import Data.List (uncons)

unsnoc :: [a] -> Maybe ([a], a)
unsnoc [] = Nothing
unsnoc [x] = Just ([], x)
unsnoc (x:xs) = (fmap.first) (x:) (unsnoc xs)

oisdk

{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, GADTs #-}

import Control.Applicative
import Control.Monad
import Test.QuickCheck

newtype Search f a
  = Search { runSearch :: [f a]
  } deriving (Functor, Show, Eq, Foldable, Traversable)

oisdk

-- https://byorgey.wordpress.com/2008/04/22/list-convolutions/
(<.>) :: [a] -> [b] -> [[(a,b)]]
xs <.> ys = foldr f [] xs
  where
    f x zs = foldr (g x) id ys ([] : zs)
    g x y a (z:zs) = ((x, y) : z) : a zs
    g x y a [] = [(x, y)] : a []

oisdk

;; -*- mode: emacs-lisp -*-
;; This file is loaded by Spacemacs at startup.
;; It must be stored in your home directory.

(defun dotspacemacs/layers ()
  "Configuration Layers declaration.
You should not put any user code in this function besides modifying the variable
values."
  (setq-default
   ;; Base distribution to use. This is a layer contained in the directory

oisdk

{-# LANGUAGE DataKinds, TypeFamilies, MultiParamTypeClasses, FlexibleInstances #-}

-- Eisenberg, Richard A. “Dependent Types in Haskell: Theory and Practice.” University of Pennsylvania, 2016. https://github.com/goldfirere/thesis/raw/master/built/thesis.pdf.

data Nat = Z | S Nat

type family AppFunc f (n :: Nat) arrows where
  AppFunc f 'Z a = f a
  AppFunc f ('S n) (a -> b) = f a -> AppFunc f n b
  

oisdk

module Data.Heap where

import Data.List (unfoldr)
import Data.Foldable (foldl')

-- | A simple, unchecked pairing heap.
data Pairing a
    = E
    | T a [Pairing a]

oisdk

struct Not<A> {
  let absurd: (A) -> Never
}

enum Sum<A,B> {
  case left(A)
  case right(B)
}

struct Prod<A,B> {

oisdk

import Decidable.Equality

%default total

infixr 7 ^
(^) : Bool -> Bool -> Bool
(^) x True  = x
(^) _ False = False

infixl 4 <.>