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@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@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@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@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@gmail.com> 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 <jeffbrown.the@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@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