zanzix

-- Our data-type for signatures
data Signature a = Sig (List a) a

-- Synonym for first-order signatures
infix 4 |-
(|-) : List a -> a -> Signature a
(|-) = Sig

-- Synonym for second-order signatures
infix 4 ||-

tkersey

-- Yoneda --------------------------------------------------------------
newtype Yoneda f a = Yoneda { runYoneda :: forall b. ((a -> b) -> f b) } 

instance Functor (Yoneda f) where
  fmap f y = Yoneda (\ab -> runYoneda y (ab . f))
  
toYoneda :: Functor f => f a -> Yoneda f a
toYoneda fa = Yoneda (\f -> fmap f fa)

fromYoneda :: Yoneda f a -> f a

zanzix

infixr 5 ~~> -- Morphisms of graphs

-- | Boilerplate for recursion schemes

-- Objects are graphs 
Graph : Type -> Type 
Graph o = o -> o -> Type 

-- Morphisms are vertex-preserving transformations between graphs

zanzix

-- Profunctor composition
data CompP : (k1 -> k2 -> Type) -> (k2 -> k3 -> Type) -> k1 -> k3 -> Type where 
InComp : {k1, k2, k3 : Type} -> {a : k1} -> {b : k2} -> {c : k3} -> {p : k1 -> k2 -> Type} -> {q : k2 -> k3 -> Type} 
  -> p a b -> q b c -> CompP p q a c 

-- Natural transformations over profunctors
Nt : {k1, k2 : Type} -> {arr : t -> t -> Type} -> (k1 -> k2 -> t) -> (k1 -> k2 -> t) -> Type  
Nt f g = {a : k1} -> {b : k2} -> arr (f a b) (g a b) 

-- Category of idris functions

zanzix

infixr 5 +++
infixr 5 ***

-- A list over a type
-- data List : Type -> Type where 
--   Nil : List a 
--   (::) : a -> List a -> List a 

Graph : Type -> Type 
Graph obj = obj -> obj -> Type 

tkersey

// https://www.typescriptlang.org/play?#code/PTAEDMEMBsGcFNQAcBOB7JbYEsAu20A7UQUqIAoXATyUQBUUBXRAXlAcIGtC0B3QgbjJkQoXI0SoMWPAWKASogrVEAMRgJQrQvABu8FIOFgAItlgArdgGN8RUAEFQgCiJQAIUU1QAeRQAeOwBpXAD4NUDJQUAAfUABvUUgAcwAuUAAiaHhwXFT+UG0YJhSHAF8wiOi43ESU1JRsBIALbNz86ELXUGKDMnArG2IMrL8ggApW9rsAShTvP0CtXRQQmPDQFHhcBhRiSuq0wezA8cQusmKhXsJrWTX6pp8XUeOUl2mvXwW9QMfY1fXN7axeLJNJ1RqHPIFE6Cc49Po3eB4Bp6OauQIAYVGqzQKBmvgCwX82MIABlMrgUiNIEVJhoQuiiREiAAlO4U0AjABGL1pzHpRLe6N+fw2W2II1WTJQADoqgkNMxWOlyakyhF1QB+UBEMlZEY46XHWmS9UpFls-Uyo2rSYwoSGUDoogWK79eygQDkRK53Ig7IQACaon6sADaBJcAF1uiIAJIAWyQ0GwlkgbocAFoQm4qB540ggyFWFSaXTXAYRABRACODGwrXgV19oB8fO9OcQMfA4ALoRDeYLgX7LkCdiCUaEIgAcvAEqmbgBCOw+0CTtC4YahEYADxLrc++ntImU2BQsFwoFTuHgCfPuDQyHQ-oYlkQkBXM7nulESjhrpuUGwDJ-QAfS0BJgMva8kFwEZaRWVZLmuWxwBxHQUVHYt7Dgk1-jFCBUMWKlbVWUohAids0HAfD1kWVYRHVAA9DV7QiRC3X9NAGE5DJQJnYYRi7SkU2gaBOUgSwOEpaksNLfdeRCOSil+dVQBAE02JuHhIDwYCUJovRMKmFJ92UlS1lFQEtJ0vS0JQIjBBU2EVNwwEuxGKzcF0gi9GIiJznIpRKNADiuJ4sC6LARjmIiejsEQVd1wS4YgjI0AMnPaTCAYONOT0UIQu4+BeISEYOFLDgRg

steventroughtonsmith

//
//  VisionViewPlaygroundApp.swift
//  VisionViewPlayground
//
//  Created by Steven Troughton-Smith on 21/09/2023.
//

import SwiftUI

@main

elkraneo

sjoerdvisscher

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeApplications #-}

sjoerdvisscher

{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE UndecidableInstances #-}