effectfully

{-# LANGUAGE ConstraintKinds   #-}
{-# LANGUAGE FlexibleContexts  #-}
{-# LANGUAGE ViewPatterns      #-}

-- This module will only define functions in Accelerate, so sometimes it is
-- useful to use the following two extensions. In particular, this allows us to
-- use the usual if-then-else syntax with Accelerate Acc and Exp terms, rather
-- than `(|?)` and `(?)` (or `acond` and `cond`) respectively.
--
{-# LANGUAGE RebindableSyntax  #-}

effectfully

infixl 3 <+>

class Proapplicative p where
  constant :: b -> p Void b
  (<+>) :: p a (c -> d) -> p b c -> p (Either a b) d

instance Proapplicative (Forget r) where
  constant _ = Forget $ \nonsense -> case nonsense of {}

  Forget f <+> Forget g = Forget $ either f g

effectfully

module CkPrim where

open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Nat.Base
open import Data.List.Base

infixl 5 _·_
infix  4 _▷_ _◁_

effectfully

open import Data.Sum
open import Data.Nat.Base

mutual
  data M (A : Set) : Set where
    r : A -> M A
    n : N -> M A

  data N : Set where
    m : M ℕ -> N

effectfully

open import Agda.Primitive using (Level; lsuc ; _⊔_)
open import Function
open import Relation.Binary.PropositionalEquality
open import Data.Product

record Magma l : Set (lsuc l) where
  field
    Carrier : Set l
    eq : Carrier → Carrier → Set l
    plus : Carrier → Carrier → Carrier

effectfully

open import Data.Unit.Base
open import Data.Nat.Base
open import Data.Product
open import Data.Vec

{-# TERMINATING #-}  -- Lie.
fix : ∀ {α} {A : Set α} -> (A -> A) -> A
fix f = f (fix f)

{-# NO_POSITIVITY_CHECK #-}

effectfully

open import Level
open import Function
open import Data.Empty
open import Data.Sum.Base

infixr 6 _⇒_
infix  3 _⊢ᵗ_ _⊢ᵗⁿᵉ_ _⊢ᵗⁿᶠ_ _⊨ᵗ_ _⊢_
infixl 9 _[_]ᵗ

module Context {α} (A : Set α) where

effectfully

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

fstFun : ∀ {A B} -> A -> B -> A
fstFun x _ = x

sndFun : ∀ {A B} -> A -> B -> B
sndFun _ y = y

uncurryFun : ∀ {A B C} -> (A -> B -> C) -> (∀ {R} -> (A -> B -> R) -> R) -> C
uncurryFun f k = f (k fstFun) (k sndFun)

effectfully

{-# LANGUAGE ConstraintKinds         #-}
{-# LANGUAGE FlexibleContexts        #-}
{-# LANGUAGE FlexibleInstances       #-}
{-# LANGUAGE FunctionalDependencies  #-}
{-# LANGUAGE InstanceSigs            #-}
{-# LANGUAGE MultiParamTypeClasses   #-}
{-# LANGUAGE RankNTypes              #-}
{-# LANGUAGE ScopedTypeVariables     #-}
{-# LANGUAGE TypeFamilies            #-}
{-# LANGUAGE TypeOperators           #-}

effectfully

-- In this article we'll show how to define data types in a PlutusIR-like language and describe
-- the problem that arises when we try to construct a generic fold over such data types.
-- This is not a tutorial on how to encode System F-omega in Agda, nor it's a tutorial on
-- generic programming techniques.

-- Since we take denotations of data types that can be impredicative, we need to make Agda
-- impredicative as well.
{-# OPTIONS --type-in-type #-}

module DirectFold where