Icelandjack

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]

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

	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)

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

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