blob: 14178b204e9aff373aeb7a8165d513fb506ac3a5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
|
{-# LANGUAGE GADTs, InstanceSigs, DataKinds, PolyKinds, RankNTypes, LambdaCase #-}
module T7908 where
import Data.Kind (Type)
class Monad' (m :: (k -> Type) -> Type) where
return' :: c a -> m c
(>>>=) :: m c -> (forall a . c a -> m d) -> m d
(>>-) :: m c -> (forall a . c a -> d) -> d
data Nat = Z' | S' Nat
data Nat' (n :: Nat) where
Z :: Nat' Z'
S :: Nat' n -> Nat' (S' n)
data Hidden :: (k -> Type) -> Type where
Hide :: m a -> Hidden m
instance Monad' Hidden where
return' :: forall k (c :: k -> Type) (a :: k) . c a -> Hidden c
return' = Hide
(>>>=) :: forall k (c :: k -> Type) (d :: k -> Type) .
Hidden c -> (forall (a :: k) . c a -> Hidden d) -> Hidden d
Hide a >>>= f = f a
(>>-) :: forall k (c :: k -> Type) d .
Hidden c -> (forall (a :: k) . c a -> d) -> d
Hide a >>- f = f a
int2nat' 0 = return' Z
int2nat' i = (int2nat' $ i - 1) >>>= (\n -> return' $ S n)
data Fin (m :: Nat) (n :: Nat) where
Fz :: Fin (S' m) Z'
Fs :: Fin m n -> Fin (S' m) (S' n)
-- N.B. not total!
nat2fin :: Nat' f -> Hidden Nat' -> Hidden (Fin f)
nat2fin (S _) (Hide Z) = return' Fz
nat2fin (S f) n = n >>>= (\case S n -> (nat2fin f (return' n) >>>= (\fn -> return' $ Fs fn)))
fin2int :: Hidden (Fin f) -> Int
fin2int f = f >>- go
where go :: Fin f n -> Int
go Fz = 0
go (Fs f) = 1 + go f
test = fin2int (nat2fin (S $ S Z) $ return' (S Z))
|
