Lysxia

{-# LANGUAGE DeriveFunctor, DeriveTraversable, RankNTypes, ScopedTypeVariables #-}

module Example where

import Control.Lens
import Data.Functor.Foldable

data PathComponent d a = Directions d | Alt [a] deriving (Show, Functor, Foldable, Traversable)

traversePC ::

Lysxia

{-# LANGUAGE
    DeriveFunctor, DeriveFoldable, DeriveTraversable, TemplateHaskell,
    RankNTypes, LambdaCase #-}

import Data.Functor.Foldable
import Data.Functor.Foldable.TH (makeBaseFunctor)

data Tree a = Leaf a | Branch a (Tree a) (Tree a)

makeBaseFunctor ''Tree

Lysxia

import Test.QuickCheck

randomList :: Gen [Double]
randomList = do
  start <- choose (0.7 :: Double, 1.2)
  go start
    where go prev = do
            new <- choose (min 0.7 (prev-0.1), max (prev+0.1) 1.2)
            acc <- go new
            return (new : acc)

Lysxia

import Control.Monad.Random

randomList :: MonadRandom m => m [Double]
randomList = do
  start <- getRandomR (0.7 :: Double, 1.2)
  go start
    where go prev = do
            new <- getRandomR (min 0.7 (prev-0.1), max (prev+0.1) 1.2)
            acc <- go new
            return (new : acc)

Lysxia

Axiom bu : bool = unit.

Definition f : bool -> unit :=
  match bu in _ = b return bool -> b with
  | eq_refl => fun x => x
  end.

Definition g : unit -> bool :=
  match bu in _ = b return b -> bool with

Lysxia

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE CPP #-}

Lysxia

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE DeriveFoldable #-}

import Control.Monad
import Data.Foldable

data Entry a = Any | Every a | Exactly a | Many [a]
    deriving (Eq, Ord, Show, Functor, Foldable, Traversable)

Lysxia

Set Implicit Arguments.
Set Contextual Implicit.

Notation TyCon := (Type -> Type).

Inductive Prog {T : Type} (sig : T -> Type -> TyCon) (a : Type) : Type :=
| Ret : a -> Prog sig a
| Op (t : T) : (forall b, sig t a b -> Prog sig b) -> Prog sig a
.

Lysxia

Require Import Coq.Logic.FunctionalExtensionality.
Require Import Coq.Program.Equality.

Class HContainer : Type :=
  {
    Shape : Type;
    Pos : Shape -> Type;
    Ctx : forall s : Shape, Pos s -> Type -> Type;
  }.

Lysxia

(* Nope, not structurally decreasing *)
Fail Fixpoint f (x y : nat) :=
  match x with
  | O => O
  | S x' => f y x'
  end.

(* But looking at f, we can define its domain inductively.
   This is literally "the set of x and y for which f is defined",