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

[Jeffrey Brown]

After further study I believe existentials are not (at least alone) enough
to solve the problem.

They do allow a heterogeneous graph type to be defined and populated:

    :set -XExistentialQuantification
    import Data.Graph.Inductive
    import Data.Maybe as Maybe

    data ShowBox = forall s. Show s => SB s
    instance Show ShowBox where show (SB x) = "SB: " ++ show x
    type ExQuantGraph = Gr ShowBox String
    let g = insNode (0, SB 1)
            $ insNode (1, SB 'a')
            $ empty :: ExQuantGraph

And once you've loaded those ShowBoxes, you can retrieve them:

    getSB :: ExQuantGraph -> Node -> ShowBox
    getSB g n = Maybe.fromJust $ lab g n

But you can't unwrap them. The following:

    getInt :: ShowBox -> Int
    getInt (SB i) = i

will not compile, because it cannot infer that i is an Int:

    todo/existentials.hs:19:21:
        Couldn't match expected type ‘Int’ with actual type ‘s’
          ‘s’ is a rigid type variable bound by
              a pattern with constructor
                SB :: forall s. Show s => s -> ShowBox,
              in an equation for ‘getInt’
              at todo/existentials.hs:19:13
        Relevant bindings include
          i :: s (bound at todo/existentials.hs:19:16)
        In the expression: i
        In an equation for ‘getInt’: getInt (SB i) = i
    Failed, modules loaded: none.


On Fri, Feb 19, 2016 at 2:12 PM, Gesh <gesh at gesh.uni.cx> wrote:

> On February 19, 2016 10:54:11 PM GMT+02:00, Francesco Ariis <
> fa-ml at ariis.it> wrote:
> >hey Gesh,
> >
> >you are right (not able to compile it atm too, but it looks
> >correct and way elegant).
> >Maybe post it in the Ml to help OP?
> >
> >ciao ciao
> >F
> >
> >
> >On Fri, Feb 19, 2016 at 04:59:56PM +0200, Gesh wrote:
> >> I'm away from compiler at the moment, but...
> >> Shouldn't this work?
> >> > {-# LANGUAGE GADTs #-}
> >> > data NodeS = HamsterS | PersonS
> >> > data NodeP a where
> >> >   Hamster :: String -> NodeP HamsterS
> >> >   Person :: String -> NodeP PersonS
> >> > data Node = forall a. NodeP a
> >> > type Graph = Gr Node...
> >> > hamsters :: NodeP PersonS -> ...
> >>
> >> Basically the idea of that you reify the choice of constructor to the
> >type level, permitting static restriction of the constructors used.
> >>
> >> HTH,
> >> Gesh
>
> Oops, meant to send to list.
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>



-- 
Jeffrey Benjamin Brown
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160220/70a00380/attachment.html>