Lysxia

(* A trick to print the simplified type of something *)

Definition type_of {A : Type} (a : A) : Type := A.
Arguments type_of _ /.
Notation simpl_type_of a := ltac:(let A := eval simpl in (type_of a) in exact A).

(* Example *)

Parameter p : forall x, 3 + x = x.

Lysxia

{- counter.hs: count comments and lines of code in .lagda.md files.

Usage:

  cat src/*.lagda.md|runghc counter.hs

Counting method:
Triple backticks either start or end a code block.
Triple backtick lines are not counted.
Code lines starting with `--` are counted as comments

Lysxia

{-# LANGUAGE DeriveFunctor, DeriveFoldable, DeriveTraversable, TypeFamilies, TemplateHaskell #-}

import Data.Functor.Foldable
import Data.Functor.Foldable.TH
import Data.Functor.Compose

-- Example type
data Exp
  = IntValue Int
  | Sum Exp Exp

Lysxia

-- Q: How to fix the last two commented lines?
--
-- Summary: Two intrinsically typed calculi A and B, and a translation from A to B.
-- The translation consists of a translation on types, followed by a translation on terms
-- indexed by the translation on types.
-- Agda won't let me case-split in the translation of (term) variables.
--
-- Signs of trouble:
-- - green slime in _A.∋_ and _B.∋_
-- - with clauses (rather than only pattern-matching on arguments)

Lysxia

{-# LANGUAGE
  DataKinds,
  DeriveGeneric,
  PolyKinds,
  StandaloneDeriving,
  TypeFamilies,
  UndecidableInstances #-}
module T where

import Data.Kind (Constraint, Type)

Lysxia

{-# LANGUAGE RankNTypes, GADTs #-}
module O where

data Coyoneda g a where
  Coyoneda :: forall g a x. g x -> (x -> a) -> Coyoneda g a

newtype Obj f g = Obj { unObj :: forall a. f a -> Coyoneda g (a, Obj f g) }

compose :: Obj f g -> Obj g h -> Obj f h
compose (Obj a) (Obj b) = Obj (\f ->

Lysxia

From Coq Require Import List.
Import ListNotations.

Inductive bintree : Type :=
  | Leaf : bintree
  | Node : bintree -> nat -> bintree -> bintree.

Inductive tree :=
  | TNode : nat -> list tree -> tree.

Lysxia

{- Derive Monad for a type like @Pipe@, which is isomorphic to a @Free@ monad

@
data Pipe i o a
  = Input (i -> Pipe i o a)
  | Output o (Pipe i o a)
  | Return a
  deriving Generic
@

Lysxia

data Freer (F : Set → Set) (A : Set) : Set₁ where
  pure : A → Freer F A
  bind : (B : Set) → F B → (B → Freer F A) → Freer F A

data Freest {A : Set} (J : A → Set) (F : A → Set) (a : A) : Set where
  pure : J a → Freest J F a
  bind : (b : A) → F b → (J b → Freest J F a) → Freest J F a

data R {A : Set} (J : A → Set) (F : A → Set) : Set → Set where
  mkR : (a : A) → F a → R J F (J a)

Lysxia

import Control.Applicative
import Control.Monad

-- Examples

example1 :: M r String ()
example1 = do
  newError "expected True"
  True <- bad
  pure ()