Lysxia

{-# LANGUAGE
  DataKinds,
  PolyKinds,
  TypeFamilies #-}
module F where

import Data.Void
import Data.Functor.Const
import Data.Kind (Type)
import GHC.TypeLits

Lysxia

-- What if...
viaTraversable :: forall t u. (Traversable t, Functor u, Foldable u, Coercible t u) => Instance (Traversable u)
viaTraversable = instance Traversable u where
  traverse f = fmap coerce . traverse @t f . coerce
  sequence = fmap coerce . sequence @t

-- then we could have DerivingVia for traversable...
deriving instance Traversable MyU = viaTraversable @MyT

Lysxia

{-# LANGUAGE GADTs, DeriveFunctor, LambdaCase #-}

import Data.Functor.Product
import Data.Void
import Control.Applicative

type Tag = String
type Attr = String

data HTML

Lysxia

{-# LANGUAGE GADTs #-}

import Data.Map (Map)
import qualified Data.Map as Map
import Control.Applicative (Applicative(..), liftA)

type Tag = String
type Forest = Map Tag Tree

data Tree = Node String Forest

Lysxia

-- Embedding of "Binders by day, labels by night" (BindersByDay.agda)
-- into "First-class names for effect handlers" (FirstClassNames.agda)
-- (syntax only)
--
-- Main idea: translate dependent name abstraction
--    ⟦ λᴺ a . M ⟧
-- to two System-F abstractions
--    Λ (η : ★) . λ (a : Ev η) . ⟦ M ⟧
-- Line 156: ⟦ ƛᴺ M ⟧ᵛ = Λ ƛ ⟦ M ⟧

Lysxia

From Coq Require Import Arith.

Axiom funext : forall (f g : nat -> bool), (forall i, f i = g i) -> f = g.

Definition is_modulus (p : (nat -> bool) -> bool) (n : nat) : Prop :=
  forall f g, (forall i, i < n -> f i = g i) -> p f = p g.

Axiom compacity : forall p, exists n, is_modulus p n.

Definition extend (b : bool) (f : nat -> bool) : nat -> bool :=

Lysxia

-- Minimax and alpha-beta pruning
--
-- Minimax can trivially be generalized to work on any lattice (@gminimax@).
-- Then alpha-beta is actually an instance of minimax.
--
-- Contents:
-- 0. Basic definitions: players and games
-- 1. Direct implementations of minimax and alpha-beta
-- 2. Generalized minimax and instantiation to alpha-beta
-- 3. QuickCheck tests

Lysxia

From Coq Require Import List Arith.
Import ListNotations.
Local Open Scope list_scope.

Inductive instr : Set :=
 | Select    : nat -> instr
 | Backspace : instr.

Definition prog := list instr.

Lysxia

{-# LANGUAGE RankNTypes, QuantifiedConstraints, PolyKinds, TypeFamilies #-}

module P where

import Data.Kind (Type)

bar :: forall g. Reflective g => g String Int Int
bar = undefined

baz :: forall g. Reflective g => Int -> g String Int Int

Lysxia

{-# LANGUAGE TypeFamilies, DataKinds, ConstraintKinds, UndecidableInstances, TypeApplications, ScopedTypeVariables #-}

module Countdown where

import Data.Proxy
import GHC.TypeNats
import Data.Kind
import qualified Fcf as F

data C2 :: Nat -> F.Exp Constraint