Icelandjack

{-
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

Icelandjack

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

Icelandjack

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

Icelandjack

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

Icelandjack

-- 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

Icelandjack

• 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 -> [a] -> SortedBy comp [a]

Icelandjack

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

Icelandjack

newtype (f `RepVia` via) a = RepVia (f a)

instance (Representable f, Coercible via (Rep f)) => Functor (f `RepVia` via) where
 fmap :: forall a b. (a -> b) -> ((f `RepVia` via) a -> (f `RepVia` via) b)
 fmap = coerce $ fmapRep @f @a @b

instance (Representable f, Coercible via (Rep f)) => Distributive (f `RepVia` via) where
 collect :: forall g a b. Functor g => (a -> (f `RepVia` via) b) -> (g a -> (f `RepVia` via) (g b))
 collect = coerce (collect @f @g @a @b)

Icelandjack

{-# Language DeriveFunctor              #-}
{-# Language DerivingVia                #-}
{-# Language FlexibleContexts           #-}
{-# Language FlexibleInstances          #-}
{-# Language GADTs                      #-}
{-# Language GeneralizedNewtypeDeriving #-}
{-# Language InstanceSigs               #-}
{-# Language ScopedTypeVariables        #-}
{-# Language TypeApplications           #-}
{-# Language TypeFamilies               #-}

Icelandjack

-- https://www.reddit.com/r/haskell/comments/abxem5/experimenting_with_kleisli_instance_of/

{-# Language TypeApplications     #-}
{-# Language RankNTypes           #-}
{-# Language DataKinds            #-}
{-# Language KindSignatures       #-}
{-# Language PolyKinds            #-}
{-# Language TypeOperators        #-}
{-# Language GADTs                #-}
{-# Language TypeFamilies         #-}