Ticket #4385: Ticket.hs

File Ticket.hs, 786 bytes (added by maltem, 7 years ago)
Line 
1{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeOperators,
2      ScopedTypeVariables, ViewPatterns, StandaloneDeriving #-}
3module Diagram where
4
5import GHC.TypeLits
6
7data Diagram (m :: Nat) (n :: Nat) where
8    Empty       :: Diagram 0 0
9    Line        :: Diagram 1 1
10    Cap         :: Diagram 0 2
11    Cup         :: Diagram 2 0
12    Above       :: Diagram m n -> Diagram n p -> Diagram m p
13    Beside      :: Diagram m n -> Diagram p q -> Diagram (m + p) (n + q)
14
15deriving instance Show (Diagram m n)
16
17addCapAbove :: Diagram 0 n -> Diagram 0 (n+2)
18addCapAbove (d :: Diagram 0 n) = Cap `Above` (Line `Beside` d `Beside` Line :: Diagram 2 (n+2))
19
20caps :: forall n. Sing (n :: Nat) -> Diagram 0 (2*n)
21caps (isZero -> IsZero)   = Empty
22caps (isZero -> IsSucc m) = addCapAbove (caps m)