[Haskell-cafe] Manual type-checking in graphs: Avoidable?

[Tom Ellis]

On Fri, Feb 19, 2016 at 05:06:57PM +0300, Kosyrev Serge wrote:
> Tom Ellis <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> writes:
> > On Fri, Feb 19, 2016 at 03:07:59PM +0300, Kosyrev Serge wrote:
> >> Tom Ellis <tom-lists-haskell-cafe-2013 at jaguarpaw.co.uk> writes:
> >> > I agree.  FGL seems inappropriate to model people owning hamsters because
> >> > you genuinely want to reflect the difference between people and hamsters by
> >> > having two different node types.
> >> 
> >> What would you propose instead?
> >
> > If I were utterly insane I would propose that FGL be extended with
> > higher-typed indexes, so instead of
> >
> >     Gr :: * -> * -> *
> >
> > we would have
> >
> >     Gr :: (k -> *) -> (k -> k -> *) -> *
> >
> > Then Hamster and Person would be the only inhabitants of some kind k, and
> > you can could choose two different types to represent them, and four
> > different types to represent the (directed) edges between them.
> 
> Richard, is something like this possible with what is in GHC 8?
> 
> Or would DataKinds already be sufficient for this?

GADTs and DataKinds already suffice for this.  Programming like this is
possible but not especially syntactically convenient, and FGL would have to
be changed throughout, of course.

(Thanks to Andras Kovacs for introducing me to this lovely world of
higher-kinded indexed types)

Tom