roboguy13

-- The algorithm here is based on the one in the paper "First-order unification by structural recursion" by Conor McBride.
-- There are some notes on the syntax in the McBride paper and how it
-- corresponds to the names here in some of the places where they differ.
--
-- The proofs are after the comment marking the beginning of the proofs.

open import Data.Nat hiding (_≤_)
import Data.Nat.Properties
import Data.Nat.Properties as ℕᵖ
open import Data.Product

roboguy13

open import Relation.Binary.PropositionalEquality
open import Data.Product

open ≡-Reasoning

module MagmaMonoid where

Associative : ∀ {A} → (A → A → A) → Set
Associative _<>_ =
  ∀ a b c →

roboguy13

-- Idea:
-- (1) Define a language of normal forms:                                                       Nf
-- (2) Define translations to and from the normal form language:                                from-Nf, to-Nf
-- (3) Show that normal forms are equal if and only if they are equal in the original language: ==→~, ~→==
-- (4) Prove the theorem about normal form language:                                            thm′
-- (5) Reflect that proof back into a statement about the original language:                    thm

open import Data.Nat
open import Data.Nat.Properties
open import Relation.Binary.PropositionalEquality renaming (subst to Eq-subst)

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

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

{-# 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

--
-- 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

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

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

import Control.Lens
import Control.Applicative

data Expr
  = Lit Int
  | Add Expr Expr

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