3

I'd like to be able to define trees using mutually inductive datatypes, and then write a generic function which can only run on certain parts of the tree, depending on what a node's descendants can be. So, for instance, if I had datatypes

data A = A1 B | A2 C D
newtype B = B String
newtype C = C String
newtype D = D Int

I want to be able to define a HasString predicate and a function getString like this:

getString :: (HasString x) => x -> String

such that HasString is satisfied for A1, B, and C, but not for D.

The standard way to do this sort of thing is just with a manual traversal:

class GetString t where
  getString :: t -> String

instance GetString B where
    getString (B s) = s

-- .... instances for A, C

In writing this out, we've basically created a proof that every A transitively contains a String.

Now, I want to do this using generic machinery, so I can get it to run on datatypes other than A. And I care about things other than getString too.

Currently, I can construct a type-level predicate that indicates whether a datatype transitively contains a String. I can even build it using generic proof machinery:

type family Or a b where
  Or True a = True
  Or a True = True
  Or a b    = False

type family And a b where
  And True True = True
  And a    b    = False

type family BaseHasString f where
  BaseHasString B = True
  BaseHasString C = True
  BaseHasString x = False

type family Has f t where
  Has f A  = Or (f A) (And (Has f B) (Or (Has f C) (Has f D)))
  Has f x  = f x

type HasString t :: Constraint = (Has BaseHasString t ~ True)

(I should also be able to generalize this further using GHC Generics.)

However, now that I have my HasString predicate, I can't figure out how to actually use it.

So, how can I write my getString function?

Cactus
  • 27,075
  • 9
  • 69
  • 149
James Koppel
  • 1,587
  • 1
  • 10
  • 16
  • All you've done is lift this to the type level. The problem is that unless you also encode some information in your data types at the type level, this is useless (since you can't reliably lift values to the type level yet). – Alec Aug 28 '16 at 23:09
  • To be clearer, the way to use your `HasString` requires you to have a lifted version of `A`, `B`, `C` and `D`, but there is currently now way to go from value -> type in general. – Alec Aug 28 '16 at 23:14
  • 2
    [Don't](http://stackoverflow.com/questions/39002342/adding-an-ord-instance-to-singleton-package-generated-naturals/39003151#39003151) [use](http://stackoverflow.com/questions/33270639/so-whats-the-point) [type](http://stackoverflow.com/questions/37923470/is-there-any-connection-between-a-b-and-a-b-true/37925725#37925725)-[level](http://stackoverflow.com/questions/38290067/idiomatic-boolean-equality-usage-singletons/38293546#38293546) [Boolean](http://stackoverflow.com/questions/38209817/checking-if-one-type-level-list-contains-another/38221146#38221146) predicates! How many times! – Benjamin Hodgson Aug 28 '16 at 23:38

0 Answers0