Constraining Constructors in a Signature

Question

So, I'm working on a fun experiment in contextual meaning and I'm running into a wall. I'm trying to define a data type that can either be a primitive or a function that transforms from one constructor to another. ``` data WeaponPart = WInt Int | WHash (Map.Map String Int) | WNull | WTrans (WeaponPart -> WeaponPart) instance Show WeaponPart where show (WInt x) = "WInt " ++ (show x) show (WHash x) = "WHash " ++ (show x) show (WTrans _) = "WTrans" show WNull = "WNull" cold :: WeaponPart -> WeaponPart cold (WInt x) = WHash (Map.singleton "frost" x) cold (WHash x) = WHash $ Map.insertWith (+) "frost" 5 x cold (WTrans x) = cold $ x (WInt 5) cold (WNull) = cold $ (WInt 5) ofTheAbyss :: WeaponPart -> WeaponPart ofTheAbyss (WTrans x) = x (WTrans x) ``` The problems is that the signature for `ofTheAbyss` allows any WeaponPart as an argument, whereas I only want to allow WTrans-constructred arguments. You can see I've only written a pattern match for that case. I've tried doing with with GADTs…

Accepted Answer

You can do this sort of thing with GADTs. Far be it from me to judge whether what results is a rabbit hole, but let me at least show the recipe. I'm using the new `PolyKinds` extension, but you can manage with less.

First, decide what sorts of stuff you will need, and define a datatype of those sorts.

```
data Sort = Base | Compound
```

Next, define your data indexed by their sorts. It's like building a little typed language.

```
data WeaponPart :: Sort -> * where
  WInt    :: Int ->                                   WeaponPart Base
  WHash   :: Map.Map String Int ->                    WeaponPart Base
  WNull   ::                                          WeaponPart Base
  WTrans  :: (Some WeaponPart -> Some WeaponPart) ->  WeaponPart Compound
```

You can represent ‘data of any sort’ via existential quantification, as follows:

```
data Some p where
  Wit :: p x -> Some p
```

Note that the `x` does not escape, but we can still inspect the ‘evidence’ that `x` ‘satisfies’ `p`. Note that `Some` must be a `data`type, not a `newtype` as GHC objects to existential `newtype`s.

You are now free to write `Sort`-generic operations. If you have generic inputs, you can just use polymorphism, effectively currying `Some p -> ...` as `forall x. p x -> ...`.

```
instance Show (WeaponPart x) where
  show (WInt x)    = "WInt " ++ (show x)
  show (WHash x)   = "WHash " ++ (show x)
  show (WTrans _)  = "WTrans"
  show WNull       = "WNull"
```

The existential is needed for `Sort`-generic outputs: here I use it for input and output.

```
cold :: Some WeaponPart -> Some WeaponPart
cold (Wit (WInt x))    = Wit (WHash (Map.singleton "frost" x))
cold (Wit (WHash x))   = Wit (WHash $ Map.insertWith (+) "frost" 5 x)
cold (Wit (WTrans x))  = cold $ x (Wit (WInt 5))
cold (Wit WNull)       = cold $ Wit (WInt 5)
```

I had to add the occasional touch of `Wit` about the place, but it's the same program.

Meanwhile, we can now write

```
ofTheAbyss :: WeaponPart Compound -> Some WeaponPart
ofTheAbyss (WTrans x) = x (Wit (WTrans x))
```

So it's not horrendous to work with embedded type systems. Sometimes there is a cost: if you want your embedded language to have subsorting, you may find you do extra computation just to change the index of some data's type, making no difference to the data themselves. If you don't need subsorting, the extra discipline can often be a real friend.

Constraining Constructors in a Signature

Solution

Problem