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

## intervals.txt
An exploration of "small-ratio" musical intervals, compared to equal temperament.  Each interval has
a perfect ratio before the colon, and a number of semitones with a cents (100th of a semitone) correction
approximation.

This is study for playing the Haken Continuum.


Root:    1   : 0
P2:     9/8  : 2 +3c
Fourth: 4/3  : 5 -2c

## gist:7611127
{-# LANGUAGE RankNTypes #-}

import Data.Foldable
import Data.Monoid

newtype M a = M { getM :: forall m. Monoid m => (a -> m) -> m }

instance Monoid (M a) where
    mempty = M $ const mempty
    x `mappend` y = M $ \f -> getM x f `mappend` getM y f

## gist:6640808
{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, FunctionalDependencies #-}

class FromCon k a | a -> k where
    convert :: k b => b -> a

instance FromCon Integral Integer where
    convert = fromIntegral

foo :: Integer
foo = convert 4
	{-# 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
	An exploration of "small-ratio" musical intervals, compared to equal temperament. Each interval has
	a perfect ratio before the colon, and a number of semitones with a cents (100th of a semitone) correction
	approximation.

	This is study for playing the Haken Continuum.


	Root: 1 : 0
	P2: 9/8 : 2 +3c
	Fourth: 4/3 : 5 -2c
	{-# LANGUAGE RankNTypes #-}

	import Data.Foldable
	import Data.Monoid

	newtype M a = M { getM :: forall m. Monoid m => (a -> m) -> m }

	instance Monoid (M a) where
	mempty = M $ const mempty
	x `mappend` y = M $ \f -> getM x f `mappend` getM y f
	{-# LANGUAGE ConstraintKinds, MultiParamTypeClasses, FunctionalDependencies #-}

	class FromCon k a \| a -> k where
	convert :: k b => b -> a

	instance FromCon Integral Integer where
	convert = fromIntegral

	foo :: Integer
	foo = convert 4