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

[Benno Fünfstück]

Hi Jeffrey,

what you want to do is not possible with the graph type that you say FGL
provides. FGL simply requires that all node types have to be equal, so it
can't preserve the information that your graph is biparite, no matter what
language features you use to define the node type.

Benno

Benjamin Edwards <edwards.benj at gmail.com> schrieb am So., 21. Feb. 2016 um
12:30 Uhr:

> 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
>>
> _______________________________________________
> 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/20160221/99815920/attachment.html>