Re: [Haskell-cafe] Manual type-checking in graphs: Avoidable?
On February 19, 2016 10:54:11 PM GMT+02:00, Francesco Ariis <fa-ml@ariis.it> 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.
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 <gesh@gesh.uni.cx> wrote:
On February 19, 2016 10:54:11 PM GMT+02:00, Francesco Ariis < fa-ml@ariis.it> 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 Haskell-Cafe@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
-- Jeffrey Benjamin Brown
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, Косырев Сергей
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
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
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 <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
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/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 <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
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/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 <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
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/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 <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
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@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@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/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 <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
participants (6)
-
Benjamin Edwards -
Benno Fünfstück -
Gesh -
Jeffrey Brown -
Kosyrev Serge -
Matt