This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module naryapplicative where | |
open import Agda.Primitive | |
module Functor | |
where | |
record functor { ℓ } (f : Set ℓ → Set ℓ) : Set (lsuc ℓ) | |
where | |
field |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
zipr = tabulate . zipf . bimap index index | |
huskr = tabulate . huskf | |
Right unit law | |
--- | |
map2 huskr > zipr > map runit_fwd | |
= {definitions} | |
map2 (tabulate < huskf) > (tabulate < zipf < bimap index index) > map runit_fwd |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE LambdaCase, DeriveGeneric #-} | |
module Examples.Biparsing.JSON where | |
import MyPrelude hiding (exponent) | |
import GHC.Generics | |
import GHC.Natural | |
import Data.List.NonEmpty (NonEmpty(..)) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE LambdaCase, EmptyCase, AllowAmbiguousTypes #-} | |
module SOP.Products where | |
import MyPrelude | |
import GHC.Generics | |
import Data.Void | |
import Data.Proxy |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module ct.ct where | |
open import Agda.Primitive | |
open import Relation.Binary.PropositionalEquality using (_≡_; refl) | |
record relation (a : Set) (b : Set) : Set₁ where | |
infix 4 _~_ | |
field | |
_~_ : a → b → Set |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Resolving dependencies... | |
Build profile: -w ghc-8.6.4 -O1 | |
In order, the following will be built (use -v for more details): | |
- adtcorerep-0.0.0 (lib) (first run) | |
Configuring library for adtcorerep-0.0.0.. | |
Preprocessing library for adtcorerep-0.0.0.. | |
Building library for adtcorerep-0.0.0.. | |
[1 of 3] Compiling Foo ( src/Foo.hs, /mnt/data/depot/git/haskell/experiments/adtcorerep/dist-newstyle/build/x86_64-linux/ghc-8.6.4/adtcorerep-0.0.0/build/Foo.o ) | |
==================== Tidy Core ==================== |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Data.Record.Operations where | |
import Prelude | |
import Data.Functor.Variant (SProxy(..)) | |
import Data.Variant.Internal (RLProxy(..)) | |
import Prim.RowList (Cons, Nil, kind RowList) | |
import Type.Data.Boolean (True, False, kind Boolean) | |
import Type.Data.Symbol (class Equals) | |
import Type.Prelude (class ListToRow, class RowToList) |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# OPTIONS_GHC -Wno-name-shadowing #-} | |
{-# LANGUAGE AllowAmbiguousTypes, FunctionalDependencies #-} | |
module FinitaryContainers where | |
import Data.Proxy | |
import Data.Functor.Const | |
import Data.Functor.Identity | |
import Data.Profunctor |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
module Adjunctions where | |
data Coproduct n x | |
where | |
First :: x -> Coproduct 'Z x | |
Next :: Either (Coproduct n x) x -> Coproduct ('S n) x | |
fold :: Coproduct n x -> x | |
fold (First x) = x | |
fold (Next (Right x)) = x |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
{-# LANGUAGE DataKinds, GADTs, RankNTypes, TypeOperators #-} | |
module Traversals where | |
import Control.Monad.Free | |
type (~>) f g = forall x. f x -> g x | |
data Nat = Z | S Nat |