Yes, that is my point. Existentials cannot be unwrapped. On Sat, Feb 20, 2016 at 4:18 AM, Kosyrev Serge <_deepfire@feelingofgreen.ru> wrote:

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

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/D... On Sat, Feb 20, 2016 at 11:59 AM, Benjamin Edwards 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 wrote:

...

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

On Sat, Feb 20, 2016 at 4:18 AM, Kosyrev Serge < _deepfire@feelingofgreen.ru> wrote:

...

Jeffrey Brown 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

-- Jeffrey Benjamin 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 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 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/D...

On Sat, Feb 20, 2016 at 11:59 AM, Benjamin Edwards < edwards.benj@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 wrote:

...

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

On Sat, Feb 20, 2016 at 4:18 AM, Kosyrev Serge < _deepfire@feelingofgreen.ru> wrote:

...

Jeffrey Brown 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

-- Jeffrey Benjamin Brown

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

-- Jeffrey Benjamin Brown

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 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 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 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 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/D...

On Sat, Feb 20, 2016 at 11:59 AM, Benjamin Edwards < edwards.benj@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 wrote:

...

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

On Sat, Feb 20, 2016 at 4:18 AM, Kosyrev Serge < _deepfire@feelingofgreen.ru> wrote:

> Jeffrey Brown 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@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

-- Jeffrey Benjamin Brown

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe

-- Jeffrey Benjamin Brown

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe