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

[Matt]

The pattern I've seen is:

data Some f where
   Some :: f a -> Some f

type G = Gr (Some Box') String

Ordinarily you lose the information about the `a`, but when you have a
GADT, that allows you to recover type information. So you can match on:

f :: Some Box' -> String
f (Some (Bi i)) = show (i + 1)
f (Some (Bs s)) = s

Matt Parsons

On Sat, Feb 20, 2016 at 4:16 PM, Jeffrey Brown <jeffbrown.the at gmail.com>
wrote:

> Interesting! I have two questions.
>
> (1) Given that Graph is of kind * -> * -> *, rather than (* -> *) -> * ->
> *, how can I use a GADT? The first graph using existentials defined earlier
> in this thread looked like:
>
>     data Box = forall s. Show s => Box s
>     type ExQuantGraph = Gr Box String
>
> If instead I use a GADT:
>
>     data Box' a where
>       Bi :: Int -> Box' Int
>       Bs :: String -> Box' String
>
> then I can't define a graph on
>
>     type G = Gr Box' String
>
> because Box is not a concrete type. I could specify (Box a) for some a,
> but then I lose the polymorphism that was the purpose of the GADT.
>
> (2) Would a GADT be better than what I'm already doing? Currently I define
> a Mindmap[1] as a graph where the nodes are a wrapper type called Expr
> ("expression"):
>
>     type Mindmap = Gr Expr _ -- the edge type is irrelevant
>     data Expr = Str String | Fl Float
>               | Tplt [String] | Rel | Coll
>               | RelSpecExpr RelVarSpec deriving(Show,Read,Eq,Ord)
>
> I do a lot of pattern matching on those constructors. If I used a GADT I
> would still be pattern matching on constructors. So do GADTs offer some
> advantage?
>
> [1]
> https://github.com/JeffreyBenjaminBrown/digraphs-with-text/blob/master/src/Dwt/Graph.hs
>
> On Sat, Feb 20, 2016 at 11:59 AM, Benjamin Edwards <edwards.benj at gmail.com
> > wrote:
>
>> if you are willing to have a closed universe, you can pattern match on a
>> gadt to do do the unpacking
>>
>> On Sat, 20 Feb 2016 at 19:19 Jeffrey Brown <jeffbrown.the at gmail.com>
>> wrote:
>>
>>> Yes, that is my point. Existentials cannot be unwrapped.
>>>
>>> On Sat, Feb 20, 2016 at 4:18 AM, Kosyrev Serge <
>>> _deepfire at feelingofgreen.ru> wrote:
>>>
>>>> Jeffrey Brown <jeffbrown.the at gmail.com> writes:
>>>> > After further study I believe existentials are not (at least alone)
>>>> > enough to solve the problem.
>>>> ..
>>>> > getInt :: ShowBox -> Int
>>>> > getInt (SB i) = i
>>>> >
>>>> > will not compile, because it cannot infer that i is an Int:
>>>>
>>>> You take a value of an existentially quantified type (which means it
>>>> can be anything at all, absent some extra context) and *proclaim* it
>>>> is an integer.
>>>>
>>>> On what grounds should the compiler accept your optimistic restriction?
>>>>
>>>> --
>>>> с уважениeм / respectfully,
>>>> Косырев Сергей
>>>>
>>>
>>>
>>>
>>> --
>>> Jeffrey Benjamin Brown
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>>>
>>
>
>
> --
> Jeffrey Benjamin Brown
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20160220/8f1bb0f8/attachment.html>