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

[Jeffrey Brown]

Clever! That answers my first question, but still leaves me unmotivated.
Would GADTs allow me to offload some kind of work onto the compiler that I
currently have to do myself?

On Sat, Feb 20, 2016 at 2:00 PM, Matt <parsonsmatt at gmail.com> wrote:

> 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
>>
>>
>


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