Not a member of Pastebin yet?
Sign Up,
it unlocks many cool features!
- -- Use "uninterpreted" types to disallow pattern matching on constructors
- type Seq :: * -> * -> *
- type Tup :: * -> * -> *
- -- This also doesn't work -- djinn treats them as Void
- -- data Seq a b
- -- data Tup a b
- iden :: Seq a a
- comp :: Seq a b -> Seq b c -> Seq a c
- unit :: Seq a ()
- injl :: Seq a b -> Seq a (Either b c)
- injr :: Seq a c -> Seq a (Either b c)
- case :: Seq (Tup a c) d -> Seq (Tup b c) d -> Seq (Tup (Either a b) c) d
- pair :: Seq a b -> Seq a c -> Seq a (Tup b c)
- take :: Seq a c -> Seq (Tup a b) c
- drop :: Seq b c -> Seq (Tup a b) c
- -- I'm trying to implement things like this
- f ? Seq (Tup a c0) (Tup b c0) -> Seq (Tup a c1) (Tup c c1) -> Seq (Tup a (Tup c0 c1)) (Tup (Tup b c) (Tup c0 c1))
- comp1 ? Seq (Tup a c0) (Tup b c0) -> Seq (Tup b c1) (Tup c c1) -> Seq (Tup a (Tup c0 c1)) (Tup c (Tup c0 c1))
- -- djinn reports that iden' has a realizer, but iden'' does not
- iden' ? Seq a a
- iden'' ? Seq b b
Add Comment
Please, Sign In to add comment