roboguy13

module ModalIntuitionistic
  where

data Prop
  = V String
  | Not Prop
  | And Prop Prop
  | Or Prop Prop
  | Prop :=> Prop
  | Box Prop

roboguy13

(* NOTE: S means successor. So, "S a" means successor of a (aka a+1) *)
Lemma S_add_left :
  forall (a b : nat),
  S (a + b) = a + S b. (* This is the proposition, given as a type. This is the type signature for the lemma *)
Proof.
  (* I am using the tactic language here. Internally this generates an expression that has the type above *)
  intros. (* Bring the variables a and b into scope *)
  destruct a  (* "destruct" is similar to induction, but it does not give you an inductive hypothesis *)
    ; easy. (* "easy" is a builtin tactic that can solve very simple proof goals. The semicolon means to apply it to all subgoals generated by the previous command *)
Qed.

roboguy13

Inductive Tree (A : Type) :=
| tip : A -> Tree A
| bin : Tree A -> Tree A -> Tree A.

Fixpoint flatten {A} (t : Tree A) : list A :=
  match t with
  | tip _ x => x :: nil
  | bin _ l r => flatten l ++ flatten r
  end.

roboguy13

{-# LANGUAGE GADTs #-}

import Control.Monad

-- Note that Cmd values are perfectly "pure" values. There's nothing here that
-- makes them impure.
data Cmd a where
  PutStr :: String -> Cmd ()
  PutStrLn :: String -> Cmd ()
  ReadLn :: Cmd Int

roboguy13

{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ImpredicativeTypes #-}
{-# LANGUAGE RankNTypes #-}

import Control.Lens
import Control.Applicative

data Expr
  = Lit Int
  | Add Expr Expr

roboguy13

open import Data.Nat
open import Data.Sum
open import Data.Product
open import Relation.Nullary

module PreservationCounterexample
  where

data Type : Set where
  Boolean : Type

roboguy13

--
-- Each interpretation will have a type of the form `Expr a -> F a`.
-- These would be a natural transformations, except that Expr is not quite a functor in this case.
--

{-# LANGUAGE GADTs #-}

module ExprInterp where

data Expr a where

roboguy13

{-# LANGUAGE DeriveFunctor, GADTs, UndecidableInstances #-}

module FreeExample where

import Control.Monad
import Data.Void -- Empty type

-- ghci> ppr example1
-- "Add 1 (Sub 2 3)"
example1 :: Expr Void

roboguy13

module NumericDSL
  where

---- Example GHCi session:
-- ghci> example (10 :: Int)
-- 130
-- ghci> example (10 :: Expr)
-- Mul (Add (Lit 10) (Lit 3)) (Lit 10)

roboguy13

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality
open import Data.Product
open import Data.Sum
open import Relation.Nullary

module MonoidNat3 where

data Expr : Set where