timjb

*.agdai

timjb

{-# OPTIONS --universe-polymorphism #-}

-- this agda module depends on https://github.com/copumpkin/categories

open import Categories.Category

module Categories.InternalLanguage {o ℓ e} (C : Category o ℓ e) where

open Category C
open Equiv

timjb

module FourFunctor

data FourFunctor y = Four y y y y

-- I get the error 'No such variable a' on the last line of this function
-- definition.
traverseFourFunctor : Applicative f => (x -> f b) -> FourFunctor x -> f (FourFunctor b)
traverseFourFunctor f (Four a b c d) = [| Four (f a) (f b) (f c) (f d) |]

-- The following last lines give the exact same error:

timjb

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ImpredicativeTypes #-}

module TestEqConstraints where

fun1 :: forall a b. (Show a, Read b) => a -> b
fun1 = read . show

fun2 :: forall b. Read b => forall a. Show a => a -> b

timjb

{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE ImpredicativeTypes #-}

module ConstraintsCommutative where

type T1 = (Show a, Read a) => a -> a
type T2 = (Read a, Show a) => a -> a

fun1 :: (Show a, Read a) => a -> a

timjb

{-# LANGUAGE TypeFamilies, DataKinds, TypeOperators #-}

module HListCurry
  ( HListElim
  , hListCurry
  , example
  ) where

import Data.HList

timjb

{-# LANGUAGE GADTs, MultiParamTypeClasses, FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}

module CompLevels where

import Control.Monad (forM_)

data Z
data S n

timjb

*.txt
.DS_Store

timjb

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE PolyKinds #-}

module NTup where

data NTup (ts :: [*]) where

timjb

module Data.RealTimeQueue

-- adapted from Chris Okasaki's `Purely Functional Data Structures`, figure 7.1

%default total

data LazyVectCell : Nat -> Type -> Type where
  Nil  : LazyVectCell Z a
  (::) : (x : a) -> (xs : Lazy (LazyVectCell n a)) -> LazyVectCell (S n) a