effectfully

{-# LANGUAGE DefaultSignatures      #-}
{-# LANGUAGE FlexibleInstances      #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE MultiParamTypeClasses  #-}
{-# LANGUAGE PartialTypeSignatures  #-}
{-# LANGUAGE TypeFamilies           #-}
{-# LANGUAGE UndecidableInstances   #-}

module MapError where

effectfully

-- <a_ton_of_LANGUAGE_pragmas>.
-- <some_imports>

data SList as where
    SNil  :: SList '[]
    SCons :: Proxy a -> SList as -> SList (a ': as)

class IList as where
    slist :: SList as

effectfully

{-# LANGUAGE FlexibleContexts      #-}
{-# LANGUAGE FlexibleInstances     #-}
{-# LANGUAGE MagicHash             #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds             #-}
{-# LANGUAGE RankNTypes            #-}
{-# LANGUAGE TupleSections         #-}
{-# LANGUAGE TypeApplications      #-}
{-# LANGUAGE TypeInType            #-}
{-# LANGUAGE TypeFamilies          #-}

effectfully

fizzBuzz :: [String]
fizzBuzz
    = take 100
    . zipWith (\i -> fromMaybe (show i) . fold) [1 :: Integer ..]
    . transpose
    . map (\(skip, word) -> cycle $ replicate skip Nothing ++ [Just word])
    $ rules
  where
    every n word = (n - 1, word)

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

effectfully

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

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

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

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