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]

	infixr 80 _◦_

	_◦_ : forall {l1 l2 l3 : Level }
	{A : -> Set l1}
	{B : A -> Set l2}
	{C : (a : A) -> B a -> Set l3}
	(g : {a : A} -> (b : B a) -> C a b )
	(f : (a : A) -> B a)
	-> (a : A) -> C a (f a)
	g ◦ f = \a -> g (f a)

	norm :: Generic1 f => Summs (Rep1 f) => f ~> Summ (Rep1 f) Zero
	norm as = summs (from1 as) (Proxy @Zero)

	class Summs rep where
	type Summ rep (end :: Type -> Type) :: Type -> Type

	summs :: rep a -> Proxy end -> Summ rep end a
	skips :: Proxy rep -> end a -> Summ rep end a

	instance Summs Zero where

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