Kazark

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

module TKD where

import Control.Applicative

befunge :: (x -> y) -> (y -> (w, z)) -> x -> w
befunge f g =
    fst . g . f

Kazark

" Usage:
"   Copy this file to your ~/.vim/autoload directory.
"   :edit oldfile
"   :new newfile
"   :call wdiff#highlight(2, 1)       " wdiff#highlight(winnr1, winnr2)

let s:save_cpo = &cpo
set cpo&vim

function wdiff#highlight(Awinnr, Bwinnr)

Kazark

module NotNotLEM

%default total
%access public export

notDistributesOverEither : Not (Either a b) -> (Not a, Not b)
notDistributesOverEither neither = (notLeft neither, notRight neither) where
  notLeft : Not (Either a b) -> Not a
  notLeft neither x = neither (Left x)

Kazark

module Rubik

%default total
%access public export

||| "North", "south", "east" and "west" face orientations
data Orient = N | E | S | W

turnCW : Orient -> Orient
turnCW N = E

Kazark

%default total

data RPS = Rock | Paper | Scissors

Eq RPS where
  Rock == Rock = True
  Paper == Paper = True
  Scissors == Scissors = True
  _ == _ = False

Kazark

/// Example encoding of the shape of GADT one finds for request types
module Request =
  /// The constructors must be kept private, so that we can refine the types of
  /// the introduction rules.
  type T<'a> =
    private
    | FileExists' of string
    | ReadText' of string
    | GetCwd'

Kazark

class Nothing : Exception {}

public static class Maybe {
  public static void Nothing() => throw new Nothing();
  public static void Guard(bool cond) { if (!cond) Nothing(); }
  public static void GuardNot(bool cond) { if (cond) Nothing(); }
}

public static class TryParse {
  public static UInt32 UInt32(string x) {

Kazark

module EnvDemo

open System
open System.IO

[<Struct>]
type Nothing =
    private
    | Nothing

Kazark

module Data.ThisOrThese where

open import Data.List.Base
open import Data.List.NonEmpty
open import Relation.Binary.PropositionalEquality.Core
open import Function

-- Apparently this is called ValidatedNel in Cats.
data ThisOrThese : Set -> Set -> Set where
  These : ∀ {A B} -> List⁺ A -> ThisOrThese A B

Kazark

module Id where

open import Relation.Binary.PropositionalEquality.Core
open import Function

data Id : Set → Set where
  Itself : ∀{A} → A → Id A

fmap : ∀{A B} → (A → B) → Id A → Id B
fmap f (Itself x) = Itself (f x)