git.iko.soy/type-level-sets
on master help sign in
type-level-sets/example2.hs
30 lines 890 B history raw
1{-# LANGUAGE DataKinds, TypeOperators, TypeFamilies, GADTs, StandaloneDeriving #-}
2{-# LANGUAGE FlexibleContexts #-}
4import GHC.TypeLits
5import Data.Type.Set
7type instance Cmp (Natural n) (Natural m) = CmpNat n m
9data Natural (a :: Nat) where
10 Z :: Natural 0
11 S :: Natural n -> Natural (n + 1)
13deriving instance Show (Natural n)
15-- foo :: Set '[Natural 0, Natural 1, Natural 3]
16foo = asSet $ Ext (S Z) (Ext (S (S (S Z))) (Ext Z Empty))
18-- bar :: Set '[Natural 1, Natural 2]
19bar = asSet $ Ext (S (S Z)) (Ext (S Z) (Ext (S Z) Empty))
21-- foobar :: Set '[Natural 0, Natural 1, Natural 2, Natural 3]
22foobar = foo `union` bar
24nonMemberTest :: NonMember (Natural 0) as => Set as -> ()
25nonMemberTest set = ()
27-- nonMemberTest meep is well typed
28meep = asSet $ Ext (S Z) (Ext (S (S Z)) Empty)
29-- nonMemberTest morp is ill typed
30morp = asSet $ Ext (S Z) (Ext (S (S Z)) (Ext Z Empty))