Constraint abuse

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}

import GHC.Prim

data Mark c (d1 :: * -> Constraint) (d2 :: * -> Constraint) d t where
    Mark :: (c d1 d2, d t) => t -> Mark c d1 d2 d t

data Tree c d a where
    Leaf :: Maybe (Mark c d d d t) -> a -> Tree c d a
    Node :: Maybe (Mark c d1 d2 d t) -> Tree c d1 a -> Tree c d2 a -> Tree c d a

alterTree :: (forall c d. Tree c d a -> Tree c d a) -> Tree (~) ((~) t) a -> Tree (~) ((~) t) a
alterTree f x = f x

Constraint abuse (annotation)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}

import GHC.Prim

data Mark c (d1 :: * -> Constraint) (d2 :: * -> Constraint) d t where
    Mark :: (c d1 d2, d t) => t -> Mark c d1 d2 d t

data Tree c d a where
    OldLeaf :: (c d1 d, d1 t, d t) => a -> t -> Tree c d a
    NewLeaf :: a -> Tree c d a
    Node :: Maybe (Mark c d1 d2 d t) -> Tree c d1 a -> Tree c d2 a -> Tree c d a

alterTree :: (forall c d. Tree c d a -> Tree c d a) -> Tree (~) ((~) t) a -> Tree (~) ((~) t) a
alterTree f x = f x

Constraint abuse (annotation)

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}

import GHC.Prim

-- a predicate would suffice, but is there a universal Universal :: * -> Constraint?
data Mark c t where
    Mark :: c t t => Mark c t

data Node' t
data Leaf' t1 t2 t

data Tree c t a where
    Leaf :: Maybe (Mark c (Node' t)) -> a -> Tree c t a
    Node :: Maybe (Mark c (Leaf' t1 t2 t)) -> Tree c t1 a -> Tree c t2 a -> Tree c t a

alterTree :: (forall c t. Tree c t a -> Tree c t a) -> Tree (~) t a -> Tree (~) t a
alterTree f x = f x

Constraint abuse (with a Functor instance and example of using alterTree)

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
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}

import GHC.Prim

data Mark c t t' where
    Mark :: c t t' => Mark c t t'

data Node'
data Leaf' t1 t2

data Tree c t a where
    Leaf :: Maybe (Mark c Node' t) -> a -> Tree c t a
    Node :: Maybe (Mark c (Leaf' t1 t2) t) -> Tree c t1 a -> Tree c t2 a -> Tree c t a

alterTree :: (forall c t. Tree c t a -> Tree c t a) -> Tree (~) t a -> Tree (~) t a
alterTree f x = f x

deriving instance Show (Mark c t t')
deriving instance Show a => Show (Tree c t a)

instance Functor (Tree c t) where
   fmap f (Leaf m a) = Leaf m (f a)
   fmap f (Node m l r) = Node m (fmap f l) (fmap f r)

ex = alterTree (fmap succ) (Node (Just Mark) (Leaf (Just Mark) 1) (Leaf (Just Mark) 2))