Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
#!/usr/bin/env stack
{- stack --resolver lts-12.0 runghc -}
{-# LANGUAGE TypeFamilies, FlexibleInstances #-}
{-# LANGUAGE DataKinds, PolyKinds, KindSignatures, TypeInType #-}
{-# LANGUAGE AllowAmbiguousTypes, TypeApplications, GADTs #-}
import Prelude hiding ((.), id)
import qualified Prelude
import Data.Kind
class Category o where
type Hom o (a :: o) (b :: o) :: Type
type ValidObject o (a :: o) :: Constraint
type ValidObject o a = ()
(.) :: Hom o b c -> Hom o a b -> Hom o a c
id :: ValidObject o a => Hom o a a
instance Category Type where
type Hom Type a b = a->b
(.) = (Prelude..)
id = Prelude.id
f :: Hom Type Int Int
f 0 = 0
f n = n+1
g :: Hom Type Int Int
g = succ
h :: Hom Type Int Int
h = (.) @Type g f
main :: IO ()
main = print [h 0, h 1, h 2]
data XY = X | Y
data XYMorphism :: (XY -> XY -> *) where
X2X :: XYMorphism 'X 'X
Y2Y :: XYMorphism 'Y 'Y
X2Y :: XYMorphism 'X 'Y
Y2X :: XYMorphism 'Y 'X
class XOrY (p :: XY) where
xyId :: XYMorphism p p
instance XOrY 'X where xyId = X2X
instance XOrY 'Y where xyId = Y2Y
instance Category XY where
type Hom XY a b = XYMorphism a b
type ValidObject XY p = XOrY p
X2X . f = f
Y2Y . f = f
f . X2X = f
f . Y2Y = f
X2Y . Y2X = Y2Y
Y2X . X2Y = X2X
id = xyId
@leftaroundabout

This comment has been minimized.

Copy link
Owner Author

@leftaroundabout leftaroundabout commented Jul 10, 2019

This is a Haskell version of the Idris interface proposed in idris-lang/Idris-dev#4736

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.