Manual type-checking in graphs: Avoidable?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
25 messages Options
12
Reply | Threaded
Open this post in threaded view
|

Manual type-checking in graphs: Avoidable?

Jeffrey Brown
I use FGL, which (roughly) defines type Gr a b as a graph on nodes of type a and edges of type b.

Suppose you wanted a graph that described which people own which hamsters, knowing only their name. You would have to make node and edge types like this:
    data GraphNode = Person String | Hamster String
    data GraphEdge = Has
where the strings represent their names.

Suppose then you wanted to write a function that, given a person, returns the names of all their hamsters. To make sure the call makes sense, the function would have to first check that the input is in fact a person. Since persons and hamsters are both constructors of the same type, you can't let Haskell's robust, beautiful type-checking system distinguish them for you; you've got to write something like "case n of Person _ -> True; _ -> False".

Is there some way around writing such manual checks?

--
Jeffrey Benjamin Brown

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Francesco Ariis
On Thu, Feb 18, 2016 at 06:50:26PM -0800, Jeffrey Brown wrote:
> Suppose then you wanted to write a function that, given a person, returns
> the names of all their hamsters. To make sure the call makes sense, the
> function would have to first check that the input is in fact a person.
> Since persons and hamsters are both constructors of the same type, you
> can't let Haskell's robust, beautiful type-checking system distinguish them
> for you; you've got to write something like "case n of Person _ -> True; _
> -> False".
>
> Is there some way around writing such manual checks?

Hello Jeffrey,
    have you considered using Phantom types [1]?

[1] https://wiki.haskell.org/Phantom_type#Simple_examples
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Jeffrey Brown
I had not!

I'm not seeing how such a solution would work. The nodes in a graph all have to have the same type. If the phantom parameter distinguished two nodes, they could not be used together.

But maybe you see something there that I don't?

On Thu, Feb 18, 2016 at 8:36 PM, Francesco Ariis <[hidden email]> wrote:
On Thu, Feb 18, 2016 at 06:50:26PM -0800, Jeffrey Brown wrote:
> Suppose then you wanted to write a function that, given a person, returns
> the names of all their hamsters. To make sure the call makes sense, the
> function would have to first check that the input is in fact a person.
> Since persons and hamsters are both constructors of the same type, you
> can't let Haskell's robust, beautiful type-checking system distinguish them
> for you; you've got to write something like "case n of Person _ -> True; _
> -> False".
>
> Is there some way around writing such manual checks?

Hello Jeffrey,
    have you considered using Phantom types [1]?

[1] https://wiki.haskell.org/Phantom_type#Simple_examples
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



--
Jeffrey Benjamin Brown

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Francesco Ariis
On Thu, Feb 18, 2016 at 09:28:24PM -0800, Jeffrey Brown wrote:
> I had not!
>
> I'm not seeing how such a solution would work. The nodes in a graph all
> have to have the same type. If the phantom parameter distinguished two
> nodes, they could not be used together.
>
> But maybe you see something there that I don't?

Argh, indeed you are correct. Maybe it can be worked around with
existential quantification like this?


{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ExistentialQuantification #-}

data Person = Person
data Hamster = Hamster

data GraphNode a = P String -- hide these
                 | H String

-- coll. of vertices
data HumHamGraph = forall c . Test c => Gr [(c, c)]

findCritters :: HumHamGraph -> GraphNode Person -> GraphNode Hamster
findCritters = undefined

class Test a where
    name :: a -> String

instance Test (GraphNode Person) where
    name (P s) = s

instance Test (GraphNode Hamster) where
    name (H s) = s

toast = [(P "a,ga", H "beta"), (H "cas", P "cds")]


For sure it looks ugly :s
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Bryan Richter-2
In reply to this post by Jeffrey Brown
On Thu, Feb 18, 2016 at 06:50:26PM -0800, Jeffrey Brown wrote:

> I use FGL, which (roughly) defines type Gr a b as a graph on nodes of type
> a and edges of type b.
>
> Suppose you wanted a graph that described which people own which hamsters,
> knowing only their name. You would have to make node and edge types like
> this:
>     data GraphNode = Person String | Hamster String
>     data GraphEdge = Has
> where the strings represent their names.
>
> Suppose then you wanted to write a function that, given a person, returns
> the names of all their hamsters. To make sure the call makes sense, the
> function would have to first check that the input is in fact a person.
> Since persons and hamsters are both constructors of the same type,
Actually, I think the problem is that "String" is the same type as
"String".

Maybe this?

    data GraphNode = NodePerson Person | NodeHamster Hamster

Then you can expose an API that just accepts a Person, and let the
find-function take care of constructing the proper start value (i.e. a
NodePerson).

    personHamsters :: MyGraph -> Person -> [Hamster]
    personHamsters g p =
        ...
      where
        startNode = NodePerson p

Still, you'll have to do case evaluation at *some* point, right? If
you have two types of nodes, and you're zooming around the graph,
you'll have to stop and dereference each node to know what to do next.

At least by hiding the details behind the API, your search function
will be total.

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

signature.asc (817 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Johannes Waldmann-2
In reply to this post by Jeffrey Brown
> .. a graph that described which people own which hamsters,

This is a bipartite graph, or, a relation. You want a type like

data Rel src tgt a =
  Rel { fore :: ! ( M.Map src (M.Map tgt a) )
      , back :: ! ( M.Map tgt (M.Map src a) )
      }

where src = People, tgt = Hamster, and a = Bool.
In general, a  could be some extra weight information.

- J.W.

cf.
https://gitlab.imn.htwk-leipzig.de/waldmann/pure-matchbox/blob/master/src/Matchbox/Relation.hs

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Tom Ellis
On Fri, Feb 19, 2016 at 12:07:14PM +0100, Johannes Waldmann wrote:

> > .. a graph that described which people own which hamsters,
>
> This is a bipartite graph, or, a relation. You want a type like
>
> data Rel src tgt a =
>   Rel { fore :: ! ( M.Map src (M.Map tgt a) )
>       , back :: ! ( M.Map tgt (M.Map src a) )
>       }
>
> where src = People, tgt = Hamster, and a = Bool.

I agree.  FGL seems inappropriate to model people owning hamsters because
you genuinely want to reflect the difference between people and hamsters by
having two different node types.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Kosyrev Serge
In reply to this post by Jeffrey Brown
Jeffrey Brown <[hidden email]> writes:

> I use FGL, which (roughly) defines type Gr a b as a graph on nodes of
> type a and edges of type b.
>
> Suppose you wanted a graph that described which people own which
> hamsters, knowing only their name. You would have to make node and
> edge types like this:
> data GraphNode = Person String | Hamster String
> data GraphEdge = Has
> where the strings represent their names.
>
> Suppose then you wanted to write a function that, given a person,
> returns the names of all their hamsters. To make sure the call makes
> sense, the function would have to first check that the input is in
> fact a person. Since persons and hamsters are both constructors of the
> same type, you can't let Haskell's robust, beautiful type-checking
> system distinguish them for you; you've got to write something like
> "case n of Person _ -> True; _ -> False".

I'll allow myself to rephrase what Tom Ellis already said more strongly.

Type systems are tools for making invalid values unrepresentable.

If you find yourself in a situation where a certain solution doesn't
allow you to do that -- keep looking.

--
с уважениeм / respectfully,
Косырев Сергей
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Kosyrev Serge
In reply to this post by Tom Ellis
Tom Ellis <[hidden email]> writes:
> I agree.  FGL seems inappropriate to model people owning hamsters because
> you genuinely want to reflect the difference between people and hamsters by
> having two different node types.

What would you propose instead?

--
с уважениeм / respectfully,
Косырев Сергей
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Andrew Butterfield-2
In reply to this post by Kosyrev Serge
What you need is a Relation, not a Graph with nodes all of the same type!

For me the problem below is most easily solved using Data.Map

either use   Map Person [Hamster]
or Map Hamster [Person]
to get the most general relations (many-many)

If every Hamster has at most one owner, use Map Hamster Person


> Jeffrey Brown <[hidden email]> writes:
>> I use FGL, which (roughly) defines type Gr a b as a graph on nodes of
>> type a and edges of type b.
>>
>> Suppose you wanted a graph that described which people own which
>> hamsters, knowing only their name. You would have to make node and
>> edge types like this:
>> data GraphNode = Person String | Hamster String
>> data GraphEdge = Has
>> where the strings represent their names.
>>
>> Suppose then you wanted to write a function that, given a person,
>> returns the names of all their hamsters. To make sure the call makes
>> sense, the function would have to first check that the input is in
>> fact a person. Since persons and hamsters are both constructors of the
>> same type, you can't let Haskell's robust, beautiful type-checking
>> system distinguish them for you; you've got to write something like
>> "case n of Person _ -> True; _ -> False".
>

Andrew Butterfield
School of Computer Science & Statistics
Trinity College
Dublin 2, Ireland

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Tom Ellis
In reply to this post by Kosyrev Serge
On Fri, Feb 19, 2016 at 03:07:59PM +0300, Kosyrev Serge wrote:
> Tom Ellis <[hidden email]> writes:
> > I agree.  FGL seems inappropriate to model people owning hamsters because
> > you genuinely want to reflect the difference between people and hamsters by
> > having two different node types.
>
> What would you propose instead?

If I were utterly insane I would propose that FGL be extended with
higher-typed indexes, so instead of

    Gr :: * -> * -> *

we would have

    Gr :: (k -> *) -> (k -> k -> *) -> *

Then Hamster and Person would be the only inhabitants of some kind k, and
you can could choose two different types to represent them, and four
different types to represent the (directed) edges between them.

I would guess that most of the FGL implementation would carry over to this
setting with no change to its structure.

However, unless Jeffrey has a hard requirement to use something FGL-like,
Johannes and Andrew's suggestions will probably be fine.

Tom

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Kosyrev Serge-2
Adding Richard to CC.

Tom Ellis <[hidden email]> writes:

> On Fri, Feb 19, 2016 at 03:07:59PM +0300, Kosyrev Serge wrote:
>> Tom Ellis <[hidden email]> writes:
>> > I agree.  FGL seems inappropriate to model people owning hamsters because
>> > you genuinely want to reflect the difference between people and hamsters by
>> > having two different node types.
>>
>> What would you propose instead?
>
> If I were utterly insane I would propose that FGL be extended with
> higher-typed indexes, so instead of
>
>     Gr :: * -> * -> *
>
> we would have
>
>     Gr :: (k -> *) -> (k -> k -> *) -> *
>
> Then Hamster and Person would be the only inhabitants of some kind k, and
> you can could choose two different types to represent them, and four
> different types to represent the (directed) edges between them.

Richard, is something like this possible with what is in GHC 8?

Or would DataKinds already be sufficient for this?

--
с уважениeм / respectfully,
Косырев Сергей
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Tom Ellis
On Fri, Feb 19, 2016 at 05:06:57PM +0300, Kosyrev Serge wrote:

> Tom Ellis <[hidden email]> writes:
> > On Fri, Feb 19, 2016 at 03:07:59PM +0300, Kosyrev Serge wrote:
> >> Tom Ellis <[hidden email]> writes:
> >> > I agree.  FGL seems inappropriate to model people owning hamsters because
> >> > you genuinely want to reflect the difference between people and hamsters by
> >> > having two different node types.
> >>
> >> What would you propose instead?
> >
> > If I were utterly insane I would propose that FGL be extended with
> > higher-typed indexes, so instead of
> >
> >     Gr :: * -> * -> *
> >
> > we would have
> >
> >     Gr :: (k -> *) -> (k -> k -> *) -> *
> >
> > Then Hamster and Person would be the only inhabitants of some kind k, and
> > you can could choose two different types to represent them, and four
> > different types to represent the (directed) edges between them.
>
> Richard, is something like this possible with what is in GHC 8?
>
> Or would DataKinds already be sufficient for this?

GADTs and DataKinds already suffice for this.  Programming like this is
possible but not especially syntactically convenient, and FGL would have to
be changed throughout, of course.

(Thanks to Andras Kovacs for introducing me to this lovely world of
higher-kinded indexed types)

Tom
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Jeffrey Brown
Francesco, using existentials looks promising! I'll work on it.

Perhaps people owning hamsters is more easily represented with maps, at least in an economy in which every hamster has exactly one owner. Here is a nearly identical example that surely requires a graph:

    data GraphNode = Person String | Hamster String
    data GraphEdge = Owns -- people own hamsters
      | Friend -- any two GraphNodes can be friends

If you used maps for this kind of information, you would have a lot of copies of the same thing. If you changed someone's name, you would have to search through each map to find every instance of it. In a graph, by contrast, you would just change it in the one place that it is represented. Moreover, with maps there's the risk of indicating someone owns a hamster that does not exist. You have to keep some kind of master record of which hamsters are available, and check each map against it. In a graph, a hamster that does not exist is not represented, and so cannot be linked to.

Bryan Richter wrote; 

> Maybe this?
>
>    data GraphNode = NodePerson Person | NodeHamster Hamster

That's what I was already doing! I feel validated.

On Fri, Feb 19, 2016 at 6:18 AM, Tom Ellis <[hidden email]> wrote:
On Fri, Feb 19, 2016 at 05:06:57PM +0300, Kosyrev Serge wrote:
> Tom Ellis <[hidden email]> writes:
> > On Fri, Feb 19, 2016 at 03:07:59PM +0300, Kosyrev Serge wrote:
> >> Tom Ellis <[hidden email]> writes:
> >> > I agree.  FGL seems inappropriate to model people owning hamsters because
> >> > you genuinely want to reflect the difference between people and hamsters by
> >> > having two different node types.
> >>
> >> What would you propose instead?
> >
> > If I were utterly insane I would propose that FGL be extended with
> > higher-typed indexes, so instead of
> >
> >     Gr :: * -> * -> *
> >
> > we would have
> >
> >     Gr :: (k -> *) -> (k -> k -> *) -> *
> >
> > Then Hamster and Person would be the only inhabitants of some kind k, and
> > you can could choose two different types to represent them, and four
> > different types to represent the (directed) edges between them.
>
> Richard, is something like this possible with what is in GHC 8?
>
> Or would DataKinds already be sufficient for this?

GADTs and DataKinds already suffice for this.  Programming like this is
possible but not especially syntactically convenient, and FGL would have to
be changed throughout, of course.

(Thanks to Andras Kovacs for introducing me to this lovely world of
higher-kinded indexed types)

Tom
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



--
Jeffrey Benjamin Brown

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Gesh
In reply to this post by Francesco Ariis
On February 19, 2016 10:54:11 PM GMT+02:00, Francesco Ariis <[hidden email]> wrote:

>hey Gesh,
>
>you are right (not able to compile it atm too, but it looks
>correct and way elegant).
>Maybe post it in the Ml to help OP?
>
>ciao ciao
>F
>
>
>On Fri, Feb 19, 2016 at 04:59:56PM +0200, Gesh wrote:
>> I'm away from compiler at the moment, but...
>> Shouldn't this work?
>> > {-# LANGUAGE GADTs #-}
>> > data NodeS = HamsterS | PersonS
>> > data NodeP a where
>> >   Hamster :: String -> NodeP HamsterS
>> >   Person :: String -> NodeP PersonS
>> > data Node = forall a. NodeP a
>> > type Graph = Gr Node...
>> > hamsters :: NodeP PersonS -> ...
>>
>> Basically the idea of that you reify the choice of constructor to the
>type level, permitting static restriction of the constructors used.
>>
>> HTH,
>> Gesh

Oops, meant to send to list.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Jeffrey Brown
After further study I believe existentials are not (at least alone) enough to solve the problem.

They do allow a heterogeneous graph type to be defined and populated:

    :set -XExistentialQuantification 
    import Data.Graph.Inductive
    import Data.Maybe as Maybe

    data ShowBox = forall s. Show s => SB s
    instance Show ShowBox where show (SB x) = "SB: " ++ show x
    type ExQuantGraph = Gr ShowBox String
    let g = insNode (0, SB 1) 
            $ insNode (1, SB 'a') 
            $ empty :: ExQuantGraph

And once you've loaded those ShowBoxes, you can retrieve them:

    getSB :: ExQuantGraph -> Node -> ShowBox
    getSB g n = Maybe.fromJust $ lab g n

But you can't unwrap them. The following:

    getInt :: ShowBox -> Int
    getInt (SB i) = i

will not compile, because it cannot infer that i is an Int:

    todo/existentials.hs:19:21:
        Couldn't match expected type ‘Int’ with actual type ‘s’
          ‘s’ is a rigid type variable bound by
              a pattern with constructor
                SB :: forall s. Show s => s -> ShowBox,
              in an equation for ‘getInt’
              at todo/existentials.hs:19:13
        Relevant bindings include
          i :: s (bound at todo/existentials.hs:19:16)
        In the expression: i
        In an equation for ‘getInt’: getInt (SB i) = i
    Failed, modules loaded: none.


On Fri, Feb 19, 2016 at 2:12 PM, Gesh <[hidden email]> wrote:
On February 19, 2016 10:54:11 PM GMT+02:00, Francesco Ariis <[hidden email]> wrote:
>hey Gesh,
>
>you are right (not able to compile it atm too, but it looks
>correct and way elegant).
>Maybe post it in the Ml to help OP?
>
>ciao ciao
>F
>
>
>On Fri, Feb 19, 2016 at 04:59:56PM +0200, Gesh wrote:
>> I'm away from compiler at the moment, but...
>> Shouldn't this work?
>> > {-# LANGUAGE GADTs #-}
>> > data NodeS = HamsterS | PersonS
>> > data NodeP a where
>> >   Hamster :: String -> NodeP HamsterS
>> >   Person :: String -> NodeP PersonS
>> > data Node = forall a. NodeP a
>> > type Graph = Gr Node...
>> > hamsters :: NodeP PersonS -> ...
>>
>> Basically the idea of that you reify the choice of constructor to the
>type level, permitting static restriction of the constructors used.
>>
>> HTH,
>> Gesh

Oops, meant to send to list.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



--
Jeffrey Benjamin Brown

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Kosyrev Serge
Jeffrey Brown <[hidden email]> 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,
Косырев Сергей
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Jeffrey Brown
Yes, that is my point. Existentials cannot be unwrapped.

On Sat, Feb 20, 2016 at 4:18 AM, Kosyrev Serge <[hidden email]> wrote:
Jeffrey Brown <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Benjamin Edwards
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 <[hidden email]> wrote:
Yes, that is my point. Existentials cannot be unwrapped.

On Sat, Feb 20, 2016 at 4:18 AM, Kosyrev Serge <[hidden email]> wrote:
Jeffrey Brown <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: Manual type-checking in graphs: Avoidable?

Jeffrey Brown
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?


On Sat, Feb 20, 2016 at 11:59 AM, Benjamin Edwards <[hidden email]> 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 <[hidden email]> wrote:
Yes, that is my point. Existentials cannot be unwrapped.

On Sat, Feb 20, 2016 at 4:18 AM, Kosyrev Serge <[hidden email]> wrote:
Jeffrey Brown <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe



--
Jeffrey Benjamin Brown

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
12