blob: 85e737a479eadc48c75d38bd4e7650c2d95bfa92 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
|
{-# Language RankNTypes #-}
{-# Language TypeApplications #-}
{-# Language DataKinds #-}
{-# Language PolyKinds #-}
{-# Language GADTs #-}
{-# Language TypeFamilies #-}
import Data.Kind
class Ríki (ob :: Type) where
type Hom :: ob -> ob -> Type
data
Kl_kind :: forall ob . (ob -> ob) -> ob -> Type where
Kl :: k -> Kl_kind (m :: ob -> ob) k
type family
UnKl (kl :: Kl_kind m k) = (res :: k) where
UnKl (Kl a) = a
|
