AndrasKovacs

{-# language Strict, BangPatterns #-}

data Tm = Var Int | App Tm Tm | Lam Tm | Fix Tm deriving (Show, Eq)
data Val = VVar Int | VApp Val Val | VLam [Val] Tm | VFix [Val] Tm

isCanonical :: Val -> Bool
isCanonical VLam{} = True
isCanonical _      = False

eval :: [Val] -> Tm -> Val

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

{-# LANGUAGE
  TypeInType, UndecidableInstances, TypeOperators, GADTs, TypeFamilies #-}

import Data.Kind
import GHC.Prim
import Data.Proxy

data Fun a b
type a ~> b = Fun a b -> Type
infixr 0 ~>

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)

AndrasKovacs

{-# LANGUAGE
  UndecidableInstances, RankNTypes, TypeOperators, TypeFamilies,
  StandaloneDeriving, DataKinds, PolyKinds, DeriveFunctor, DeriveFoldable,
  DeriveTraversable, LambdaCase, PatternSynonyms, TemplateHaskell #-}

import Control.Monad
import Control.Applicative
import Data.Singletons.TH

AndrasKovacs

-- Examples

data Foo = A | B | C

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

foo :: Foo -> Int

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

{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}

{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:

  https://github.com/ollef/sixty

The main idea is that during elaboration, we need different evaluation

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

open import Algebra
open import Data.Bool
open import Data.Empty
open import Data.List
open import Data.List.Properties
open import Data.Nat
open import Data.Product
open import Data.Unit
open import Function