AndrasKovacs

-- Examples

data Foo = A | B | C

foo :: Foo -> Int
foo A = 10
foo B
foo C = 20

foo :: Foo -> Int

AndrasKovacs

{-
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:

    "A simple and efficient implementation of strong call by need by an abstract machine"
    https://dl.acm.org/doi/10.1145/3549822

This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.

AndrasKovacs

{-# OPTIONS --type-in-type #-}

open import Relation.Binary.PropositionalEquality
  renaming (cong to ap; sym to infixl 6 _⁻¹; subst to tr; trans to infixr 4 _◾_)
open import Data.Product
  renaming (proj₁ to ₁; proj₂ to ₂)

--------------------------------------------------------------------------------

NatAlg : Set

AndrasKovacs

Require Import Coq.Unicode.Utf8.

(*
As far as I can tell, there is way more literature in Agda on datatype-generic
programming than in Coq. I think part of the reason is that the Agda literature
makes liberal use of induction-recursion and fancy termination/positivity
checking, to define fixpoints of functors. These features are not available in
Coq.

AndrasKovacs

{-# language LambdaCase, Strict, OverloadedStrings, DerivingVia #-}
{-# options_ghc -Wincomplete-patterns #-}

{-|
Simple universe polymorphism. Features:

  - Non-first-class levels: there is a distinct Pi, lambda and application for
    levels. Levels are distinct from terms in syntax/values.
  - The surface language only allows abstraction over finite levels. Internally,

AndrasKovacs

open import Relation.Binary.PropositionalEquality
  renaming (cong to ap; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; subst to tr)
open import Data.Empty
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)

infixr 3 _⇒_
infix  3 sort⇒_
infixl 2 _▶_
infix  2 _$_
infixr 4 _∷_ _∷'_

AndrasKovacs

open import Relation.Binary.PropositionalEquality
  renaming (cong to ap; sym to infix 6 _⁻¹; trans to infixr 5 _◾_; subst to tr)
open import Data.Empty
open import Function hiding (_$_)
open import Data.Product renaming (proj₁ to ₁; proj₂ to ₂)

infixr 3 _⇒_
infix 3 sort⇒_
infixl 2 _▶_
infixl 2 _$_ _$'_

AndrasKovacs

{-# language ScopedTypeVariables, RankNTypes, BlockArguments, TypeApplications,
    LambdaCase #-}

module Lib
    ( foldr
    ) where

import           Data.Foldable (foldl')
import           Prelude       hiding (foldr)

AndrasKovacs

{-# language Strict, LambdaCase, GADTs #-}
{-# options_ghc -Wincomplete-patterns -O2 #-}

import Gauge -- package gauge
import Control.Monad

data Op
  = Add
  | NotEq

AndrasKovacs

{-# language LambdaCase, Strict, BangPatterns, ViewPatterns, OverloadedStrings #-}
{-# options_ghc -Wincomplete-patterns #-}

module UnivPoly where

import Data.Foldable
import Data.Maybe
import Data.String
import Debug.Trace