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

[Benjamin Edwards]

Sorry Jeffrey, I haven't been following the thread too closely, I just
threw that out there as a way to recover an existential type through
pattern matching. It's a cool feature of GADTs. I'm not sure it necessarily
gets you too much in your specific problem.

On Sun, 21 Feb 2016 at 02:27 Jeffrey Brown <jeffbrown.the at gmail.com> wrote:

> 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/20160221/9339b4be/attachment-0001.html>