roboguy13

Definition assoc_law {g : Type} (op : g -> g -> g) :=
  forall (x y z : g),
    op (op x y) z = op x (op y z).

Definition left_iden_law {g : Type} (iden : g) (op : g -> g -> g) :=
  forall (x : g),
    op iden x = x.

Definition right_iden_law {g : Type} (iden : g) (op : g -> g -> g) :=
  forall (x : g),

roboguy13

-- The following lets you write:
--   ghci> both @All Proxy (Proxy :: Proxy (TyApp Maybe)) Just (1, 'a')
--   (Just 1,Just 'a')
--
-- The type involved in that example is:
--   ghci> :t both @All Proxy (Proxy :: Proxy (TyApp Maybe))
--   both @All Proxy (Proxy :: Proxy (TyApp Maybe))
--     :: (forall r x. (All x, TyApp Maybe x r) => x -> r)
--        -> (a, b) -> (Maybe a, Maybe b)

roboguy13

-- This works
--   recoverF_CPS everyP (f (A 1)) B'
-- and so does
--   recoverF_CPS (Proxy :: Proxy ((~) Char)) (\x -> case x of A _ -> 'a'; B -> 'b') (A' 1)
-- But this isn't allowed to type check:
--   recoverF_CPS everyP (f B) B'

-- Also note this law holds:
--   recoverF_CPS everyP recoverF' = id

roboguy13

{-# LANGUAGE RankNTypes #-}

exampleA :: [a] -> [a]
exampleA = reverse

exampleB :: [Int] -> [Int]
exampleB = filter even

rank2 :: (forall a. [a] -> [a]) -> [Char]
rank2 f = f "abc"

roboguy13

Inductive Eq : Type -> Type :=
  | MkEq : forall a, (a -> a -> bool) -> Eq a.

Definition my_equal {e b c : Type} {t : Type -> Type} (dict : Eq e) (f : forall a, t a -> e) (x : t b) (y : t c) : bool.
  destruct dict as [T eq].
  exact (eq (f b x) (f c y)).
Defined.

roboguy13

{-# LANGUAGE Strict #-}

{-# OPTIONS_GHC -O3 #-}

import           Data.Complex
import           Control.Applicative
import           Control.Arrow
import           Control.Monad

main :: IO ()

roboguy13

Require Import Coq.Logic.FinFun.

Theorem the_theorem
  : ~ exists (f : unit -> bool), Surjective f.
Proof.
  intro H.
  destruct H.
  destruct (H true).
  destruct (H false).
  destruct x0, x1.

roboguy13

class Budget {
    var days : array<int>
    var weeks : array<int>

    function valid() : bool
        reads this, weeks, days
    {
        days.Length == weeks.Length &&
            (forall i :: 0 <= i < days.Length ==> (weeks[i] == 7 * days[i]))
    }

roboguy13

-- GHCi example:
--   ghci > mempty @(Permutation (Nx (Nx (Nx Zr))) Int)
--   Perm ((:++) 0 ((:++) 1 ((:++) 2 EmptyVec)))

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}

roboguy13

(* https://twitter.com/codydroux/status/1570158204243288066 *)

Section Iter_to_ind.

  Variable B : Prop.
  Variable F : Prop -> Prop.

  (* F is a monad *)
  Variable fmap : forall (a b : Prop), (a -> b) -> F a -> F b.
  Variable pure : forall (a : Prop),   a -> F a.