AndrasKovacs

{-# language Strict #-}

import qualified Data.Primitive.PrimArray as A
import GHC.Exts (IsList(..))
import Data.Bits
import Data.Word

type Rule = A.PrimArray Word8

mkRule :: Word8 -> Rule

AndrasKovacs

{-# OPTIONS --postfix-projections --without-K --safe #-}

{-
Large countable ordinals in Agda. For examples, see the bottom of this file.
Checked with Agda 2.6.0.1.

Countable ordinals are useful in "big number" contests, because they
can be directly converted into fast-growing ℕ → ℕ functions via the
fast-growing hierarchy:

AndrasKovacs

{-# OPTIONS --without-K #-}

{-
Claim: finitary inductive types are constructible from Π,Σ,Uᵢ,_≡_ and ℕ, without
quotients. Sketch in two parts.

1. First, construction of finitary inductive types from Π, Σ, Uᵢ, _≡_ and binary trees.
   Here I only show this for really simple, single-sorted closed inductive types,
   but it should work for indexed inductive types as well.

AndrasKovacs

{-
Inductive-recursive universes, indexed by levels which are below an arbitrary type-theoretic ordinal number (see HoTT book 10.3). This includes all kinds of transfinite levels as well.

Checked with: Agda 2.6.1, stdlib 1.3

My original motivation was to give inductive-recursive (or equivalently: large inductive)
semantics to to Jon Sterling's cumulative algebraic TT paper:

AndrasKovacs

{-# language
  TypeInType, GADTs, RankNTypes, TypeFamilies,
  TypeOperators, TypeApplications,
  UnicodeSyntax, UndecidableInstances
#-}

import Data.Kind
import Data.Proxy

data Nat = Z | S Nat

AndrasKovacs

{-# language GADTs #-}

-- https://www.reddit.com/r/haskell/comments/9uz2f5/code_challenge_welltyped_tree_node_order/

data Tree a where
  OneT :: a -> Tree a
  Ap   :: (a -> b -> c) -> Tree a -> Tree b -> Tree c

data FunList a where

AndrasKovacs

-- https://stackoverflow.com/questions/52244800/how-to-normalize-rewrite-rules-that-always-decrease-the-inputs-size/52246261#52246261

open import Relation.Binary.PropositionalEquality
open import Data.Nat
open import Relation.Nullary
open import Data.Empty
open import Data.Star

data AB : Set where
  A : AB -> AB

AndrasKovacs

{-# language
  TypeInType, ScopedTypeVariables, RankNTypes,
  GADTs, TypeOperators, TypeApplications, BangPatterns
#-}

-- requires ghc-typelits-natnormalise
{-# options_ghc -fplugin GHC.TypeLits.Normalise #-}

{-|
Tested with ghc-8.4.3

AndrasKovacs

data Ty : Set where
  ι   : Ty
  _⇒_ : Ty → Ty → Ty
infixr 3 _⇒_

data Con : Set where
  ∙   : Con
  _▶_ : Con → Ty → Con
infixl 3 _▶_

AndrasKovacs

{-# language OverloadedStrings, UnicodeSyntax, LambdaCase,
             ViewPatterns, NoMonomorphismRestriction #-}
{-# options_ghc -fwarn-incomplete-patterns #-}

{- Minimal bidirectional dependent type checker with type-in-type. Related to Coquand's
   algorithm. #-}

import Prelude hiding (all)