Icelandjack

http://www.cs.ox.ac.uk/people/bob.coecke/AbrNikos.pdf

Why study categories—what are they good for? We can offer a range of answers for readers coming from different backgrounds:

• For mathematicians: category theory organises your previous mathematical experience in a new and powerful way, revealing new connections and structure, and allows you to “think bigger thoughts”.
• For computer scientists: category theory gives a precise handle on important notions such as compositionality, abstraction, representationindependence, genericity and more. Otherwise put, it provides the fundamental mathematical structures underpinning many key programming concepts.
• For logicians: category theory gives a syntax-independent view of the fundamental structures of logic, and opens up new kinds of models and interpretations.
• For philosophers: category theory opens up a fresh approach to structuralist foundations of mathematics and science; and an alternative to the traditional focus on set theory
• For **p

Icelandjack

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

Icelandjack

Type classes in terms of row types

type Semigroup s = { Monoid s with mappend :: s -> s -> s | _ }

type Pointed f = { Applicative f with pure  :: forall a. a -> f a | _ }
type Apply   f = { Applicative f with (<*>) :: forall a b. f (a -> b) -> f a -> f b | _ }
type Bind    m = { Monad       m with (>>=) :: forall a b. m a -> (a -> m b) -> m b | _ }

Icelandjack

HList : Sublist -> Hask

type Cat k = k -> k -> Type

data Sublist :: Cat [a] where
  Stop :: Sublist '[] '[]
  Drop :: Sublist xs ys -> Sublist (x:xs) ys
  Keep :: Sublist xs ys -> Sublist (x:xs) (x:ys)

Icelandjack

Non-standard operators I use :) linked to from my twitter profile

I use kind synonyms

type T   = Type
type TT  = T -> T
type TTT = T -> TT
type C   = Constraint
type TC  = T -> C

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

Reddit discusson thread.

I made a way to get more free stuff and free stuff is good.

The current implementation of deriveVia is here, it works with all the examples here. Needs GHC 8.2 and th-desugar.

It doesn't take long

for new Haskellers to get pampered by their compiler. For the price of a line or two the compiler offers to do your job, to write uninteresting code for you (in the form of type classes) such as equality, comparison, serialization, ... in the case of 3-D vectors

Icelandjack

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

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]