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

[Jeffrey Brown]

It is possible! Off-list, Matt Parsons explained how to do it. With his
permission I have copied that email below:


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

> Phantom types can help disambiguate:
>
> data Hamster
> data Person
>
> data Node a where
>     HNode :: String -> Node Hamster
>     PNode :: String -> Node Person
>
> type G = Gr (Some Node) String
>
> Your API functions will have the type:
>
> getPersonHamsters :: Node Person -> [Node Hamster]
> getPersonHamsters (PNode personName) = ...
>
> Since the only way to construct a `Node Person` is with the `PNode`
> constructor, you don't even have to check for the `HNode` constructor, and
> it's a type error to provide it to the function.
>
> You'll need to wrap in `Some` to store in the graph and unwrap/pattern
> match on the `Some` to get the data back out. This'll provide some
> additional safety by constraining surface area of the less-strongly-typed
> interface, but it won't take care of it entirely.
>
> Matt Parsons
>
> On Sat, Feb 20, 2016 at 9:27 PM, 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
>>
>
>


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