Luke Palmer luqui

## opaque.hs
{-# LANGUAGE RankNTypes, TypeApplications #-}

-- We give a constructive proof that any natural transformation that uses
-- a type switch in its implementation can also be implemented without the type switch,
-- as long as the domain functor is finitely Traversable (and the argument can easily
-- be modified to drop the finiteness property).

-- We do this by providing a function `opaquify` which takes an n.t. which may do
-- type switches, and returns an equivalent n.t. which does not.

## opaque.mkd

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                luqui
                / opaque.mkd
            
            
              Created
              May 23, 2020 04:32
            
              
                Natural transformations must treat their arguments opaquely
              
          
    We will give some strong evidence for the claim "natural transformations must treat their arguments opauely".
This is the best I can come up with short of defining a lambda calculus with type-switch and showing that
the type-switch can always be eliminated (which I suspect would be possible) but is too difficult.
Instead, we show that the requirement that a function be a natural transformation is invariant under encodings --
that is, if you mangle the argument in whatever way you like, and unmangle the result, you get the same
thing as if you didn't do any mangling.
Therefore, in order to a natural transformation t :: F a -> G a to make an "exception" for a type, it would have to
make the same exception for all possible encodings of that type as well.  In particular, one possible encoding is to
encode each incoming a in F as a unique integer. The resulting integers in the result G value show us exactly

  
## foldl.hs
import qualified Control.Foldl as Foldl

average :: Foldl.Fold Double Double
average = (/) <$> Foldl.sum <*> Foldl.genericLength

-- This could have been done more easily with the Foldl.scan function, but
-- I wanted to demonstrate how to access the intermediate states manually.
averages :: [Double] -> [Double]
averages xs
    | Foldl.Fold step s0 obs <- average

## higher_products.hs
{-# OPTIONS -fdefer-type-errors #-}
{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, RankNTypes, GADTs, TypeApplications, ScopedTypeVariables, UndecidableInstances, MultiParamTypeClasses, TypeInType, TypeSynonymInstances, FlexibleInstances, InstanceSigs, FlexibleContexts #-}

import Prelude hiding (id, (.))
import Control.Category
import Data.Kind (Type)
import Unsafe.Coerce
import Data.Type.Equality

type family (~>) :: k -> k -> Type

## monadcomplex.hs
-- In an alternate universe of Haskell where this worked...
data (Num a) => Complex a = a :+ a

instance Functor Complex where
    fmap f (x :+ y) = f x :+ f y

instance Monad Complex where
    return x = x :+ 0
    join ((a :+ b) :+ (c :+ d)) = (a - d) :+ (b + c)

## baseball.html
<!DOCTYPE html>
<html>
<head>
<style type="text/css">
h1 {
font-family:"Impact";
font-size: 48pt;
text-align: left;
text-indent: 48px;
color: #000;

## dragon.hs
{-# LANGUAGE RankNTypes, GADTs, ConstraintKinds, ScopedTypeVariables, DeriveFunctor #-}

import Data.Monoid
import Data.Foldable (toList)
import Data.Constraint (Dict(..))
import qualified Data.DList as DList
import qualified Data.Sequence as Seq

class (Functor f) => DragonList f where
    singleton :: a -> f a

## table.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              0 stars
            
          
                luqui
                / table.md
            
            
              Last active
              August 29, 2015 14:13
            
          
    Really? <table> isn't available in markdown?

 4

 
  1
  2
 
 
  3
  

## howtowrite.hs
import Data.List (intercalate)

write :: String -> String
write = intercalate ". " . map (\word -> "Write " ++ show word) . words

howToWrite :: String
howToWrite = "How to write this book: " ++ write howToWrite

{-
>>> putStrLn $ take 1000 howToWrite

## russell.idris
data Set : Type where
    Comp : (Set -> Type) -> Set

elt : Set -> Set -> Type
elt (Comp f) = f

W : Set
W = Comp (\A => Not (A `elt` A))

Russell : Type
	{-# LANGUAGE RankNTypes, TypeApplications #-}

	-- We give a constructive proof that any natural transformation that uses
	-- a type switch in its implementation can also be implemented without the type switch,
	-- as long as the domain functor is finitely Traversable (and the argument can easily
	-- be modified to drop the finiteness property).

	-- We do this by providing a function `opaquify` which takes an n.t. which may do
	-- type switches, and returns an equivalent n.t. which does not.
	import qualified Control.Foldl as Foldl

	average :: Foldl.Fold Double Double
	average = (/) <$> Foldl.sum <*> Foldl.genericLength

	-- This could have been done more easily with the Foldl.scan function, but
	-- I wanted to demonstrate how to access the intermediate states manually.
	averages :: [Double] -> [Double]
	averages xs
	\| Foldl.Fold step s0 obs <- average
	{-# OPTIONS -fdefer-type-errors #-}
	{-# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, RankNTypes, GADTs, TypeApplications, ScopedTypeVariables, UndecidableInstances, MultiParamTypeClasses, TypeInType, TypeSynonymInstances, FlexibleInstances, InstanceSigs, FlexibleContexts #-}

	import Prelude hiding (id, (.))
	import Control.Category
	import Data.Kind (Type)
	import Unsafe.Coerce
	import Data.Type.Equality

	type family (~>) :: k -> k -> Type
	-- In an alternate universe of Haskell where this worked...
	data (Num a) => Complex a = a :+ a

	instance Functor Complex where
	fmap f (x :+ y) = f x :+ f y

	instance Monad Complex where
	return x = x :+ 0
	join ((a :+ b) :+ (c :+ d)) = (a - d) :+ (b + c)
	<!DOCTYPE html>
	<html>
	<head>
	<style type="text/css">
	h1 {
	font-family:"Impact";
	font-size: 48pt;
	text-align: left;
	text-indent: 48px;
	color: #000;
	{-# LANGUAGE RankNTypes, GADTs, ConstraintKinds, ScopedTypeVariables, DeriveFunctor #-}

	import Data.Monoid
	import Data.Foldable (toList)
	import Data.Constraint (Dict(..))
	import qualified Data.DList as DList
	import qualified Data.Sequence as Seq

	class (Functor f) => DragonList f where
	singleton :: a -> f a
	import Data.List (intercalate)

	write :: String -> String
	write = intercalate ". " . map (\word -> "Write " ++ show word) . words

	howToWrite :: String
	howToWrite = "How to write this book: " ++ write howToWrite

	{-
	>>> putStrLn $ take 1000 howToWrite
	data Set : Type where
	Comp : (Set -> Type) -> Set

	elt : Set -> Set -> Type
	elt (Comp f) = f

	W : Set
	W = Comp (\A => Not (A `elt` A))

	Russell : Type