morganstanley/hobbes

It is unclear how to use the Map typeclass

Opened this issue · 4 comments

I've got a couple simple typeclass things working, but the code below fails, and I don't see why

class AddOne a b | a -> b where
addOne :: a -> b

instance AddOne int int where
addOne x = x + 1

instance (Map a b c d e f g h, AddOne c d) => AddOne f h where
addOne x = fmap(addOne, x)

Since we have both
instance () => Map d c a b 'array' [a] 'array' [b]
instance AddOne int int

it would seem that we should be able to resolve AddOne [int] [int]
But addOne([1]) fails.

Sadly nothing in boot does anything of the form instance Map ... => ... so it is tricky to puzzle out.

TBH, I think we should scrap this approach to 'Map/Functor' and do something more like vanilla Haskell.

The current implementation came out of the experience we got building programs with structural types where we were very enthusiastic about the additional power that structural reasoning gave us. This went a little bit too far in the case of 'Map' where we basically had to infer an intended nominal type from a structural one, and that's not possible in general.

Rather than distinguishing certain structural patterns like this, we should just overload on type constructors in the usual way (and we already have a way to map type constructors with arguments into structural types if we need that information for something else).

That will make these puzzles much less difficult to solve and more straightforward to reason about the error messages that come up.

We still need to be a little bit more general than in Haskell, because for example if you map a function over a stored sequence, you don't want the result (necessarily) to itself be a stored sequence.

PS: I'm curious to know if you've looked at the structural type constraints, they will let you avoid a lot of boilerplate you might otherwise have to handle with something like Template Haskell (and IMHO e.g. fix the awkwardness of record types in Haskell).

FWIW, one way to recover something like Haskell's Functor would be like:

$ cat t.hob

class Functor f a b where
    fm :: (a -> b, (f a)) -> (f b)

data A x = [x]

mkA :: [x] -> (A x)
mkA = unsafeCast

unA :: ((A x)) -> [x]
unA = unsafeCast

instance Functor A a b where
    fm f xs = mkA(map(f,unA(xs)))

instance (Show x) => Show (A x) where
    show x = show(unA(x))

So that e.g.:

$ hi -s t.hob
> fm(show,mkA([1..10]))
["1", "2", "3", "4", "5", "6", "7", "8", "9", "10"]

It wouldn't be a lot of work to refactor things this way, but as described earlier this approach has some problems as in e.g. the case of querying out of structured data files (where we don't want the result structure to itself be a stored type, though the source structure must be).

But it's enough to define the class you want:

$ cat t.hob
...
class AddOne t where
    addOne :: t -> t

instance AddOne int where
    addOne x = x + 1

instance (Functor f t t, AddOne t) => AddOne (f t) where
    addOne x = fm(addOne,x)

So that:

> addOne(mkA([mkA([1..10]), mkA([11..20])]))
[[2, 3, 4, 5, 6, 7, 8, 9, 10, 11], [12, 13, 14, 15, 16, 17, 18, 19, 20, 21]]

HTH

Thanks, this helps in understanding what is going on. The structural typing is very nice, as you say it gets rid of the need of a lot of boilerplate, although I'm still not totally certain that this ease isn't going to bite me later.

If it helps (in case the point wasn't made clearly elsewhere), the typical win for structural types is in writing explicit instance generators where you'd otherwise rely on implicit magic with "deriving".

For example, when you make custom record types in Haskell you might rely on "deriving Eq" to get equality testing. But you can generically deconstruct record types this way to make the obvious definition:

instance (r={a*rr}, Eq a, Eq rr) => Eq r where
  x === y = recordHeadValue(x) === recordHeadValue(y) and recordTail(x) === recordTail(y)

So that two instances of a record are equal if all of their fields are equal. It's the same thing you'd get with "deriving Eq" in Haskell but now the tools are in your hands to make the "deriving" logic yourself (and that tool is just plain old type classes).

Where I've found that you can get in trouble with structural types (where I've got in trouble) is in designating a "meaning" to a particular structure when that structure isn't canonical. The bits you found with Map are a good example of that (maybe the most complicated example). Another one would be using ()+t to mean maybe t because you could just as easily have picked t+() (similarly ^x.(()+(a*x)) to mean list a because it could just as easily have been ^x.((a*x)+()) for the same reason).

IMHO this is not a bug with structural types per se, but just a "user error" (one I've made a few times as I've come to terms with having this tool available myself). In hindsight, I think that the right approach is to make structural types the default and introduce "intentional types" to designate these cases where you have some intention where you pick a structural representation arbitrarily.

Does that make sense? I think you can still do what you do in Haskell, but don't have to resort to Template Haskell (or avoid it out of exhaustion) and can also do obvious things like have two struct types with overlapping field names in the same module, ditto for variants.