Icelandjack

## classless.hs
{-# Language EmptyCase                #-}
{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language PatternSynonyms          #-}
{-# Language PolyKinds                #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}
{-# Language TypeFamilies             #-}
{-# Language TypeOperators            #-}

## Ran.markdown

      
              1 file
            
          
              0 forks
            
          
              18 comments
            
          
              3 stars
            
          
                Icelandjack
                / Ran.markdown
            
            
              Last active
              November 13, 2020 20:51
            
              
                Right Kan extensions and Indexed Monads
              
          
    reddit discussion

IxMonad implies Monad for (EDIT: Exists as LowerIx with newtype LiftIx m i j a = LiftIx (m a))
and `
newtype Same :: (k -> k -> k' -> Type) -> (k -> k' -> Type) where
  Same :: p f f a -> Same p f a

  
## Functor.hs
{-
Every functor is a function mapping categories.

I want to specify them all in one place,

  instance Functor (->) where
    type Arr (->) = (<–) :- (->) :- End (->)

without having to specified partial applications of it

## circ.hs
instance (Applicative f, Treey tree) => Treey (Ap f tree) where
 leaf :: Int -> Ap f tree
 leaf = pure . leaf

 (¦) :: Ap f tree -> Ap f tree -> Ap f tree
 (¦) = liftA2 (¦)

instance (Biapplicative bi, Treey tree1, Treey tree2) => Treey (Biap bi tree1 tree2) where
 leaf :: Int -> Biap bi tree1 tree2
 leaf = liftA2 bipure leaf leaf

## showelem.hs
data SVec :: forall n a. Vec n a -> Type where
 SVecO :: SVec VecO
 SVecS :: Sing a -> SVec as -> SVec (a :> as)

type instance Sing @(Vec n a) = SVec @n @a

instance SingI VecO where
 sing :: Sing VecO
 sing = SVecO

## On.hs
{-# Language DataKinds                #-}
{-# Language DerivingVia              #-}
{-# Language FlexibleInstances        #-}
{-# Language GADTs                    #-}
{-# Language InstanceSigs             #-}
{-# Language PolyKinds                #-}
{-# Language RankNTypes               #-}
{-# Language ScopedTypeVariables      #-}
{-# Language StandaloneKindSignatures #-}
{-# Language TypeApplications         #-}

## OpenKinds.markdown

      
              1 file
            
          
              0 forks
            
          
              7 comments
            
          
              8 stars
            
          
                Icelandjack
                / OpenKinds.markdown
            
            
              Last active
              January 26, 2020 20:53
            
              
                Rethinking Tricky Classes: Explicit Witnesses of Monoid Actions, Semigroup / Monoid / Applicative homomorphisms
              
          
    Reddit discussion

Continuation of Encoding Overlapping, Extensible Isomorphisms:
encoding "open kinds" to better express some awkward type classes.

  
## GhostsViaDepartedProofs.md

      
              1 file
            
          
              0 forks
            
          
              0 comments
            
          
              1 star
            
          
                Icelandjack
                / GhostsViaDepartedProofs.md
            
            
              Last active
              November 10, 2019 15:46
            
              
                Ghosts Via Departed Proofs
              
          
Riff on https://www.reddit.com/r/haskell/comments/8qn0wr/safe_api_design_with_ghosts_of_departed_proofs/
reddit thread: https://www.reddit.com/r/haskell/comments/dlzc46/ghosts_via_departed_proofs_experimenting/

Ghosts of Departed Proofs introduces sortBy. It sorts using a comparison function a -> a -> Ordering named "comp". The name is then recorded in the return type: "this list is sorted by comp"!
type Cmp :: Type -> Type
type Cmp a = (a -> a -> Ordering)

sortBy :: Cmp a~~comp -&gt; [a] -&gt; SortedBy comp [a]

  
## state.hs
-- https://stackoverflow.com/questions/49587122/type-variable-location-in-transformers

{-# Language DerivingVia #-}

import Control.Applicative
import Control.Monad.State
import Data.Functor.Compose
import Data.Functor.Identity

-- >> :instances StateT _ IO

## Text.Read.Lex.isSymbolChar
!#$%&*+-./:<=>?@\^|~¡¢£¤¥¦§¨©¬®¯°±´¶·¸¿×÷˂˃˄˅˒˓˔˕˖˗˘˙˚˛˜˝˞˟˥˦˧˨˩˪˫˭˯˰˱˲˳˴˵˶˷˸˹˺˻˼˽˾˿͵;΄΅·϶҂՚՛՜՝՞՟։֊֍֎֏־׀׃׆׳״؆؇؈؉؊؋،؍؎؏؛؞؟٪٫٬٭۔۞۩۽۾܀܁܂܃܄܅܆܇܈܉܊܋܌܍߶߷߸߹࠰࠱࠲࠳࠴࠵࠶࠷࠸࠹࠺࠻࠼࠽࠾࡞।॥॰৲৳৺৻૰૱୰௳௴௵௶௷௸௹௺౿൹෴฿๏๚๛༁༂༃༄༅༆༇༈༉༊་༌།༎༏༐༑༒༓༔༕༖༗༚༛༜༝༞༟༴༶༸྅྾྿࿀࿁࿂࿃࿄࿅࿇࿈࿉࿊࿋࿌࿎࿏࿐࿑࿒࿓࿔࿕࿖࿗࿘࿙࿚၊။၌၍၎၏႞႟჻፠፡።፣፤፥፦፧፨᎐᎑᎒᎓᎔᎕᎖᎗᎘᎙᐀᙭᙮᛫᛬᛭᜵᜶។៕៖៘៙៚៛᠀᠁᠂᠃᠄᠅᠆᠇᠈᠉᠊᥀᥄᥅᧞᧟᧠᧡᧢᧣᧤᧥᧦᧧᧨᧩᧪᧫᧬᧭᧮᧯᧰᧱᧲᧳᧴᧵᧶᧷᧸᧹᧺᧻᧼᧽᧾᧿᨞᨟᪠᪡᪢᪣᪤᪥᪦᪨᪩᪪᪫᪬᪭᭚᭛᭜᭝᭞᭟᭠᭡᭢᭣᭤᭥᭦᭧᭨᭩᭪᭴᭵᭶᭷᭸᭹᭺᭻᭼᯼᯽᯾᯿᰻᰼᰽᰾᰿᱾᱿᳀᳁᳂᳃᳄᳅᳆᳇᳓᾽᾿῀῁῍῎῏῝῞῟῭΅`´῾‐‑‒–—―‖‗†‡•‣․‥…‧‰‱′″‴‵‶‷‸※‼‽‾‿⁀⁁⁂⁃⁄⁇⁈⁉⁊⁋⁌⁍⁎⁏⁐⁑⁒⁓⁔⁕⁖⁗⁘⁙⁚⁛⁜⁝⁞⁺⁻⁼₊₋₌₠₡₢₣₤₥₦₧₨₩₪₫€₭₮₯₰₱₲₳₴₵₶₷₸₹₺₻₼₽℀℁℃℄℅℆℈℉℔№℗℘℞℟℠℡™℣℥℧℩℮℺℻⅀⅁⅂⅃⅄⅊⅋⅌⅍⅏←↑→↓↔↕↖↗↘↙↚↛↜↝↞↟↠↡↢↣↤↥↦↧↨↩↪↫↬↭↮↯↰↱↲↳↴↵↶↷↸↹↺↻↼↽↾↿⇀⇁⇂⇃⇄⇅⇆⇇⇈⇉⇊⇋⇌⇍⇎⇏⇐⇑⇒⇓⇔⇕⇖⇗⇘⇙⇚⇛⇜⇝⇞⇟⇠⇡⇢⇣⇤⇥⇦⇧⇨⇩⇪⇫⇬⇭⇮⇯⇰⇱⇲⇳⇴⇵⇶⇷⇸⇹⇺⇻⇼⇽⇾⇿∀∁∂∃∄∅∆∇∈∉∊∋∌∍∎∏∐∑−∓∔∕∖∗∘∙√∛∜∝∞∟∠∡∢∣∤∥∦∧∨∩∪∫∬∭∮∯∰∱∲∳∴∵∶∷∸∹∺∻∼∽∾∿≀≁≂≃≄≅≆≇≈≉≊≋≌≍≎≏≐≑≒≓≔≕≖≗≘≙≚≛≜≝≞≟≠≡≢≣≤≥≦≧≨≩≪≫≬≭≮≯≰≱≲≳≴≵≶≷≸≹≺≻≼≽≾≿⊀⊁⊂⊃⊄⊅⊆⊇⊈⊉⊊⊋⊌⊍⊎⊏⊐⊑⊒⊓⊔⊕⊖⊗⊘⊙⊚⊛⊜⊝⊞⊟⊠⊡⊢⊣⊤⊥⊦⊧⊨⊩⊪⊫⊬⊭⊮⊯⊰⊱⊲⊳⊴⊵⊶⊷⊸⊹⊺⊻⊼⊽⊾⊿⋀⋁⋂⋃⋄⋅⋆⋇⋈⋉⋊⋋⋌⋍⋎⋏⋐⋑⋒⋓⋔⋕⋖⋗⋘⋙⋚⋛⋜⋝⋞⋟⋠⋡⋢⋣⋤⋥⋦⋧⋨⋩⋪⋫⋬⋭⋮⋯⋰⋱⋲⋳⋴⋵⋶⋷⋸⋹⋺⋻⋼⋽⋾⋿⌀⌁⌂⌃⌄⌅⌆⌇⌌⌍⌎⌏⌐⌑⌒⌓⌔⌕⌖⌗⌘⌙⌚⌛⌜⌝⌞⌟⌠⌡⌢⌣⌤⌥⌦⌧⌨⌫⌬⌭⌮⌯⌰⌱⌲⌳⌴⌵⌶⌷⌸⌹⌺⌻⌼⌽⌾⌿⍀⍁⍂⍃⍄⍅⍆⍇⍈⍉⍊⍋⍌⍍⍎⍏⍐⍑⍒⍓⍔⍕⍖⍗⍘⍙⍚⍛⍜⍝⍞⍟⍠⍡⍢⍣⍤⍥⍦⍧⍨⍩⍪⍫⍬⍭⍮⍯⍰⍱⍲⍳⍴
	{-# Language EmptyCase #-}
	{-# Language GADTs #-}
	{-# Language InstanceSigs #-}
	{-# Language PatternSynonyms #-}
	{-# Language PolyKinds #-}
	{-# Language ScopedTypeVariables #-}
	{-# Language StandaloneKindSignatures #-}
	{-# Language TypeApplications #-}
	{-# Language TypeFamilies #-}
	{-# Language TypeOperators #-}
	{-
	Every functor is a function mapping categories.

	I want to specify them all in one place,

	instance Functor (->) where
	type Arr (->) = (<–) :- (->) :- End (->)

	without having to specified partial applications of it
	instance (Applicative f, Treey tree) => Treey (Ap f tree) where
	leaf :: Int -> Ap f tree
	leaf = pure . leaf

	(¦) :: Ap f tree -> Ap f tree -> Ap f tree
	(¦) = liftA2 (¦)

	instance (Biapplicative bi, Treey tree1, Treey tree2) => Treey (Biap bi tree1 tree2) where
	leaf :: Int -> Biap bi tree1 tree2
	leaf = liftA2 bipure leaf leaf
	data SVec :: forall n a. Vec n a -> Type where
	SVecO :: SVec VecO
	SVecS :: Sing a -> SVec as -> SVec (a :> as)

	type instance Sing @(Vec n a) = SVec @n @a

	instance SingI VecO where
	sing :: Sing VecO
	sing = SVecO
	{-# Language DataKinds #-}
	{-# Language DerivingVia #-}
	{-# Language FlexibleInstances #-}
	{-# Language GADTs #-}
	{-# Language InstanceSigs #-}
	{-# Language PolyKinds #-}
	{-# Language RankNTypes #-}
	{-# Language ScopedTypeVariables #-}
	{-# Language StandaloneKindSignatures #-}
	{-# Language TypeApplications #-}
	-- https://stackoverflow.com/questions/49587122/type-variable-location-in-transformers

	{-# Language DerivingVia #-}

	import Control.Applicative
	import Control.Monad.State
	import Data.Functor.Compose
	import Data.Functor.Identity

	-- >> :instances StateT _ IO