working my way through Data.Type.Equality...my head hurts...
Full code here… https://github.com/goldfirere/nyc-hug-oct2014/blob/master/Equality.hs Lets start at the beginning… Ø data a :~: b where Ø Refl :: a :~: a Looks reasonable….” a :~: b” is inhabited by 1 value…of type “a :~: a” Ø sym :: (a :~: b) -> (b :~: a) Ø sym Refl = Refl hmmm… (a :~: b) implies that a is b so (b :~: a) brilliant Ø -- | Transitivity of equality Ø trans :: (a :~: b) -> (b :~: c) -> (a :~: c) Ø trans Refl Refl = Refl Ø -- | Type-safe cast, using propositional equality Ø castWith :: (a :~: b) -> a -> b Ø castWith Refl x = x fine…. But…. Ø -- | Generalized form of type-safe cast using propositional equality Ø gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r Ø gcastWith Refl x = x I don’t even understand the signature What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a” What would a value of type “((a ~ b) => r)” look like? CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
On Tue, Jan 13, 2015 at 12:39 PM, Nicholls, Mark
But….
Ø -- | Generalized form of type-safe cast using propositional equality
Ø gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
Ø gcastWith Refl x = x
I don’t even understand the signature
What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a”
a ~ b is a constraint that a and b are exactly the same type. For example, Int ~ Int is satisfiable, but Int ~ Bool is not. So what gcastWith does is take a witness that a and b are the same type (witnessed by the a :~: b value), and then lets you form a value using that evidence. What would a value of type “((a ~ b) => r)” look like?
I can't come up with a workable example right now, but I could imagine that you might have: reverseReverse :: a :~: (Reverse (Reverse a)) Then if you have something that needs to work on a Reverse (Reverse a) value, but you only have a 'a' around, you can show GHC that it doesn't matter - because they are the same type: gcastWith reverseReverse :: (a ~ Reverse (Reverse a) => r) -> r Presumably whatever 'r' is will refer to 'a' and do something with it (maybe mapping over a list or something). Sorry that this is all fairly vague, but hopefully that gives you some leads. -- ocharles
It is fairly vague…I think it gets me to understand in a hand wavy sort of way.
Let me look a little deeper.
On Tue, Jan 13, 2015 at 12:39 PM, Nicholls, Mark
-- | Generalized form of type-safe cast using propositional equality
gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r
gcastWith Refl x = x
I don’t even understand the signature What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a” a ~ b is a constraint that a and b are exactly the same type. For example, Int ~ Int is satisfiable, but Int ~ Bool is not. So what gcastWith does is take a witness that a and b are the same type (witnessed by the a :~: b value), and then lets you form a value using that evidence. What would a value of type “((a ~ b) => r)” look like? I can't come up with a workable example right now, but I could imagine that you might have: reverseReverse :: a :~: (Reverse (Reverse a)) Then if you have something that needs to work on a Reverse (Reverse a) value, but you only have a 'a' around, you can show GHC that it doesn't matter - because they are the same type: gcastWith reverseReverse :: (a ~ Reverse (Reverse a) => r) -> r Presumably whatever 'r' is will refer to 'a' and do something with it (maybe mapping over a list or something). Sorry that this is all fairly vague, but hopefully that gives you some leads. -- ocharles CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)…. It means GHC knows that two types are equal.
and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a” Yeah, that looks scary. You use gcastWith when you need a value of type a but you have a value of type b with a proof that a and b are equal (here a proof is a value of a :~: b). I have a practical example, though perhaps it's not the simplest one:
https://github.com/jstolarek/dep-typed-wbl-heaps-hs/blob/master/src/TwoPassM... This code is thought as an intermediate level tutorial - you might want to give it a try. Another example I have is here (I use the name subst, but it's identical to gcastWith): https://github.com/jstolarek/why-dependent-types-matter/blob/master/WhyDepen... HTH Janek
brilliant the 1st link is a bit challenging...the 2nd I can probably cope with for the moment, though I may be asking questions. If you have any beginner level tutorial, then that’s even better..I can just about cope with associated types, type families and GADT...some of the other extensions I suspect disbelief for.
What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)…. It means GHC knows that two types are equal.
and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a” Yeah, that looks scary. You use gcastWith when you need a value of type a but you have a value of type b with a proof that a and b are equal (here a proof is a value of a :~: b). I have a practical example, though perhaps it's not the simplest one:
https://github.com/jstolarek/dep-typed-wbl-heaps-hs/blob/master/src/TwoPassM... This code is thought as an intermediate level tutorial - you might want to give it a try. Another example I have is here (I use the name subst, but it's identical to gcastWith): https://github.com/jstolarek/why-dependent-types-matter/blob/master/WhyDepen... HTH Janek CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
the 1st link is a bit challenging... You may want to read 3rd chapter of Okasaki's "Purely Functional Data Structures" - it describes weight-biased lefitsh heaps without any type-level magic.
the 2nd I can probably cope with for the moment, though I may be asking questions. As you probably noticed this is based on paper "Why Dependent Types Matter", so you should probably read the paper and follow the code.
If you have any beginner level tutorial, then that’s even better.. I personally learned all these things in Agda. It's a bit easier because it's a fully-fledged dependently-typed language and things are just easier to write. Only then I moved to Haskell.
Janek
I can just about cope with associated types, type families and GADT...some of the other extensions I suspect disbelief for.
What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….
It means GHC knows that two types are equal.
and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a”
Yeah, that looks scary. You use gcastWith when you need a value of type a but you have a value of type b with a proof that a and b are equal (here a proof is a value of a :~: b). I have a practical example, though perhaps it's not the simplest one:
https://github.com/jstolarek/dep-typed-wbl-heaps-hs/blob/master/src/TwoPass Merge/RankProof.hs#L361
This code is thought as an intermediate level tutorial - you might want to give it a try. Another example I have is here (I use the name subst, but it's identical to gcastWith):
https://github.com/jstolarek/why-dependent-types-matter/blob/master/WhyDepe ndentTypesMatter.hs#L220
HTH
Janek
CONFIDENTIALITY NOTICE
This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited.
While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data.
Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us.
MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
I was thinking of doing it the other way around.... i.e. get my head around Haskell....then around Haskell's type system extensions....then look at agda. CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
It can be done that way, but just keep in mind that a lot of things are
significantly more complicated than they need to be in Haskell, when
compared to Agda. Idris might be a good option to explore too, as you get
very familiar syntax, but something that's designed from the start for
dependent typing.
On Tue, Jan 13, 2015 at 2:10 PM, Nicholls, Mark
I was thinking of doing it the other way around.... i.e. get my head around Haskell....then around Haskell's type system extensions....then look at agda.
CONFIDENTIALITY NOTICE
This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited.
While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data.
Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us.
MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Why not, if you feel that works for you. But in Agda you don't need things like Type Families or some fancy encodings like singletons - you can use the same functions at term and type levels. Janek Dnia wtorek, 13 stycznia 2015, Nicholls, Mark napisał:
I was thinking of doing it the other way around.... i.e. get my head around Haskell....then around Haskell's type system extensions....then look at agda.
CONFIDENTIALITY NOTICE
This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited.
While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data.
Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us.
MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
Hmmm scanning the paper I think it easier to read the code and follow the paper. The paper is a little intractable.
the 1st link is a bit challenging... You may want to read 3rd chapter of Okasaki's "Purely Functional Data Structures" - it describes weight-biased lefitsh heaps without any type-level magic.
the 2nd I can probably cope with for the moment, though I may be asking questions. As you probably noticed this is based on paper "Why Dependent Types Matter", so you should probably read the paper and follow the code.
If you have any beginner level tutorial, then that’s even better.. I personally learned all these things in Agda. It's a bit easier because it's a fully-fledged dependently-typed language and things are just easier to write. Only then I moved to Haskell.
Janek
I can just about cope with associated types, type families and GADT...some of the other extensions I suspect disbelief for.
What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….
It means GHC knows that two types are equal.
and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a”
Yeah, that looks scary. You use gcastWith when you need a value of type a but you have a value of type b with a proof that a and b are equal (here a proof is a value of a :~: b). I have a practical example, though perhaps it's not the simplest one:
https://github.com/jstolarek/dep-typed-wbl-heaps-hs/blob/master/src/Two Pass Merge/RankProof.hs#L361
This code is thought as an intermediate level tutorial - you might want to give it a try. Another example I have is here (I use the name subst, but it's identical to gcastWith):
https://github.com/jstolarek/why-dependent-types-matter/blob/master/Why Depe ndentTypesMatter.hs#L220
HTH
Janek
CONFIDENTIALITY NOTICE
This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited.
While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data.
Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us.
MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
Nicholls, Mark
Full code here… https://github.com/goldfirere/nyc-hug-oct2014/blob/master/Equality.hs
... That's a very good question. Apart from a reference in the ghc manual, I have been unable to find a reference for "~". It doesn't exist in the Haskell 2010 Language Report, it didn’t exist in ghc 6.8.2 but made an appearance in 7.0.1. The documentation in the manual is rather sparse and doesn’t contain a reference: https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf section 7.11. Folk on #ghc referred me to http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/. I can find papers that refer to ~ in F_C (aka FC?) but as far as I can tell not in the Haskell language itself. Apparently: They were introduced as part of the System Fc rewrite. The Fc approach has the benefit of unifying a lot of the work on GADTs, functional dependencies, type and data families, etc. all behind the scenes. Every once in a while, (~) constraints can leak into the surface language and it can be useful to be able to talk about them in the surface language of Haskell, because otherwise it isn't clear how to talk about F a ~ G b style constraints, which arise in practice when you work with type families. I don't know if this is correct way to think about them but I think of ":~:" as internal equality and "~" as external equality and gcastWith allows you to use a proof using internal equality to discharge a proof of external equality. For example suppose you have a type family
type family (n :: Nat) :+ (m :: Nat) :: Nat where Z :+ m = m S n :+ m = n :+ S m
and a proof
plus_id_r :: SNat n -> ((n :+ Z) :~: n)
then you could use this with a definition of a vector
data Vec a n where Nil :: Vec a Z (:::) :: a -> Vec a n -> Vec a (S n)
to prove
elim0 :: SNat n -> (Vec a (n :+ Z) -> Vec a n) elim0 n x = gcastWith (plus_id_r n) x
PS Nat and SNat are the usual natural numbers and singleton.
Hmmm ok And what is a singleton type!...I think this is a phrase I have chosen to ignore up to now.
Full code here… https://github.com/goldfirere/nyc-hug-oct2014/blob/master/Equality.hs
... That's a very good question. Apart from a reference in the ghc manual, I have been unable to find a reference for "~". It doesn't exist in the Haskell 2010 Language Report, it didn’t exist in ghc 6.8.2 but made an appearance in 7.0.1. The documentation in the manual is rather sparse and doesn’t contain a reference: https://downloads.haskell.org/~ghc/latest/docs/users_guide.pdf section 7.11. Folk on #ghc referred me to http://research.microsoft.com/en-us/um/people/simonpj/papers/ext-f/. I can find papers that refer to ~ in F_C (aka FC?) but as far as I can tell not in the Haskell language itself. Apparently: They were introduced as part of the System Fc rewrite. The Fc approach has the benefit of unifying a lot of the work on GADTs, functional dependencies, type and data families, etc. all behind the scenes. Every once in a while, (~) constraints can leak into the surface language and it can be useful to be able to talk about them in the surface language of Haskell, because otherwise it isn't clear how to talk about F a ~ G b style constraints, which arise in practice when you work with type families. I don't know if this is correct way to think about them but I think of ":~:" as internal equality and "~" as external equality and gcastWith allows you to use a proof using internal equality to discharge a proof of external equality. For example suppose you have a type family
type family (n :: Nat) :+ (m :: Nat) :: Nat where Z :+ m = m S n :+ m = n :+ S m
and a proof
plus_id_r :: SNat n -> ((n :+ Z) :~: n)
then you could use this with a definition of a vector
data Vec a n where Nil :: Vec a Z (:::) :: a -> Vec a n -> Vec a (S n)
to prove
elim0 :: SNat n -> (Vec a (n :+ Z) -> Vec a n) elim0 n x = gcastWith (plus_id_r n) x
PS Nat and SNat are the usual natural numbers and singleton. _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
Hi Mark,
Permit me to take a stab from the beginning.
On Jan 13, 2015, at 7:39 AM, "Nicholls, Mark"
Full code here… https://github.com/goldfirere/nyc-hug-oct2014/blob/master/Equality.hs
First off, I should point out that Data.Type.Equality, while indeed served at the address above, is now a standard library. The code in that repo is identical to the version that ships with GHC 7.8.
Lets start at the beginning…
Ø data a :~: b where Ø Refl :: a :~: a
Looks reasonable….” a :~: b” is inhabited by 1 value…of type “a :~: a”
This is true, but there's a bit more going on. If, say, we learn that the type `foo :~: bar` is indeed inhabited by `Refl`, then we know that `foo` and `bar` are the same types. That is
baz :: foo :~: bar -> ... baz evidence = case evidence of Refl -> -- here, we may assume that `foo` and `bar` are fully identical
Conversely, whenever we *use* `Refl` in an expression, we must know that the two types being related are indeed equal.
Ø sym :: (a :~: b) -> (b :~: a) Ø sym Refl = Refl
hmmm… (a :~: b) implies that a is b so (b :~: a) brilliant
Yes. After pattern-matching on `Refl`, GHC learns that `a` is identical to `b`. Thus, when we use `Refl` on the right-hand side, we know `b` is the same as `a`, and thus the use of `Refl` type checks.
Ø -- | Transitivity of equality Ø trans :: (a :~: b) -> (b :~: c) -> (a :~: c) Ø trans Refl Refl = Refl
Ø -- | Type-safe cast, using propositional equality Ø castWith :: (a :~: b) -> a -> b Ø castWith Refl x = x
fine….
But….
Ø -- | Generalized form of type-safe cast using propositional equality Ø gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r Ø gcastWith Refl x = x
I don’t even understand the signature
What does “~” mean…(it’s something that comes out in error messages when my types are all messed up)….and then there’s a “=>” going on…in the middle of a signature….I know “=>” in the context of “Num a => a -> a -> a”
While the comments I've seen about `~` are quite true, I think there's a simpler way to explain it. `~` is simply equality on types. The constraint `a ~ b` means that `a` is the same type as `b`. We could have spelled it `=` if that weren't used elsewhere. Before `~` was added to GHC, it might have been implemented like this:
class Equals a b | a -> b, b -> a instance Equals x x -- no other instances!
The proper `~` works better in type inference than this functional-dependency approach, but perhaps rewriting `~` in terms of functional dependencies is illuminating. When a constraint `a ~ b` is in the context, then GHC assumes the types are the same, and freely rewrites one to the other. The type `(a ~ b) => r` above is a higher-rank type, which is why it may look strange to you. Let's skip the precise definition of "higher-rank" for now. In practical terms: let's say you write `gcastWith proof x` in your program. By the type signature of `gcastWith`, GHC knows that `proof` must have type `a :~: b` for some `a` and `b`. It further knows that `x` has the type `(a ~ b) => r`, for some `r`, but the same `a` and `b`. Of course, if a Haskell expression as a type `constraint => stuff`, then GHC can assume `constraint` when type-checking the expression. The same holds here: GHC assumes `a ~ b` (that is, `a` and `b` are identical) when type-checking the expression `x`. Perhaps, somewhere deep inside `x`, you pass a variable of type `a` to a function expecting a `b` -- that's just fine, because `a` and `b` are the same. The `r` type variable in the type of `gcastWith` is the type of the result. It's the type you would naively give to `x`, but without a particular assumption that `a` and `b` are the same.
What would a value of type “((a ~ b) => r)” look like?
It looks just like a value of type `r`. Except that GHC has an extra assumption during type-checking. Contrast this to, say,
min :: Ord a => a -> a -> a min = \x y -> if x < y then x else y
What does a value of `Ord a => a -> a -> a` look like? Identically to a value of type `a -> a -> a`, except with an extra assumption. This is just like the type `(a ~ b) => r`, just less exotic-looking. As for singleton types and dependent types: they're great fun, but I don't think you need to go anywhere near there to understand this module. (Other modules in that repo, on the other hand, get scarier...)
I hope this helps! Richard
Brilliant!
Let my cogs turn....slowly...
I think the problem I will have writing these proofs, is how much the compiler "knows" at a given point is not especially clear....you have to build a mental model of what its doing.
Interesting stuff though.
From: Richard Eisenberg [mailto:eir@cis.upenn.edu]
Sent: 13 January 2015 5:13 PM
To: Nicholls, Mark
Cc: haskell-cafe
Subject: Re: [Haskell-cafe] working my way through Data.Type.Equality...my head hurts...
Hi Mark,
Permit me to take a stab from the beginning.
On Jan 13, 2015, at 7:39 AM, "Nicholls, Mark"
data a :~: b where Refl :: a :~: a
Looks reasonable...." a :~: b" is inhabited by 1 value...of type "a :~: a" This is true, but there's a bit more going on. If, say, we learn that the type `foo :~: bar` is indeed inhabited by `Refl`, then we know that `foo` and `bar` are the same types. That is
baz :: foo :~: bar -> ... baz evidence = case evidence of Refl -> -- here, we may assume that `foo` and `bar` are fully identical
Conversely, whenever we *use* `Refl` in an expression, we must know that the two types being related are indeed equal.
sym :: (a :~: b) -> (b :~: a) sym Refl = Refl
hmmm... (a :~: b) implies that a is b so (b :~: a) brilliant Yes. After pattern-matching on `Refl`, GHC learns that `a` is identical to `b`. Thus, when we use `Refl` on the right-hand side, we know `b` is the same as `a`, and thus the use of `Refl` type checks.
-- | Transitivity of equality trans :: (a :~: b) -> (b :~: c) -> (a :~: c) trans Refl Refl = Refl
-- | Type-safe cast, using propositional equality castWith :: (a :~: b) -> a -> b castWith Refl x = x
fine.... But....
-- | Generalized form of type-safe cast using propositional equality gcastWith :: (a :~: b) -> ((a ~ b) => r) -> r gcastWith Refl x = x
I don't even understand the signature What does "~" mean...(it's something that comes out in error messages when my types are all messed up)....and then there's a "=>" going on...in the middle of a signature....I know "=>" in the context of "Num a => a -> a -> a" While the comments I've seen about `~` are quite true, I think there's a simpler way to explain it. `~` is simply equality on types. The constraint `a ~ b` means that `a` is the same type as `b`. We could have spelled it `=` if that weren't used elsewhere. Before `~` was added to GHC, it might have been implemented like this:
class Equals a b | a -> b, b -> a instance Equals x x -- no other instances!
The proper `~` works better in type inference than this functional-dependency approach, but perhaps rewriting `~` in terms of functional dependencies is illuminating. When a constraint `a ~ b` is in the context, then GHC assumes the types are the same, and freely rewrites one to the other. The type `(a ~ b) => r` above is a higher-rank type, which is why it may look strange to you. Let's skip the precise definition of "higher-rank" for now. In practical terms: let's say you write `gcastWith proof x` in your program. By the type signature of `gcastWith`, GHC knows that `proof` must have type `a :~: b` for some `a` and `b`. It further knows that `x` has the type `(a ~ b) => r`, for some `r`, but the same `a` and `b`. Of course, if a Haskell expression as a type `constraint => stuff`, then GHC can assume `constraint` when type-checking the expression. The same holds here: GHC assumes `a ~ b` (that is, `a` and `b` are identical) when type-checking the expression `x`. Perhaps, somewhere deep inside `x`, you pass a variable of type `a` to a function expecting a `b` -- that's just fine, because `a` and `b` are the same. The `r` type variable in the type of `gcastWith` is the type of the result. It's the type you would naively give to `x`, but without a particular assumption that `a` and `b` are the same. What would a value of type "((a ~ b) => r)" look like? It looks just like a value of type `r`. Except that GHC has an extra assumption during type-checking. Contrast this to, say,
min :: Ord a => a -> a -> a min = \x y -> if x < y then x else y
What does a value of `Ord a => a -> a -> a` look like? Identically to a value of type `a -> a -> a`, except with an extra assumption. This is just like the type `(a ~ b) => r`, just less exotic-looking. As for singleton types and dependent types: they're great fun, but I don't think you need to go anywhere near there to understand this module. (Other modules in that repo, on the other hand, get scarier...) I hope this helps! Richard CONFIDENTIALITY NOTICE This e-mail (and any attached files) is confidential and protected by copyright (and other intellectual property rights). If you are not the intended recipient please e-mail the sender and then delete the email and any attached files immediately. Any further use or dissemination is prohibited. While MTV Networks Europe has taken steps to ensure that this email and any attachments are virus free, it is your responsibility to ensure that this message and any attachments are virus free and do not affect your systems / data. Communicating by email is not 100% secure and carries risks such as delay, data corruption, non-delivery, wrongful interception and unauthorised amendment. If you communicate with us by e-mail, you acknowledge and assume these risks, and you agree to take appropriate measures to minimise these risks when e-mailing us. MTV Networks International, MTV Networks UK & Ireland, Greenhouse, Nickelodeon Viacom Consumer Products, VBSi, Viacom Brand Solutions International, Be Viacom, Viacom International Media Networks and VIMN and Comedy Central are all trading names of MTV Networks Europe. MTV Networks Europe is a partnership between MTV Networks Europe Inc. and Viacom Networks Europe Inc. Address for service in Great Britain is 17-29 Hawley Crescent, London, NW1 8TT.
participants (5)
-
Dominic Steinitz -
Jan Stolarek -
Nicholls, Mark -
Oliver Charles -
Richard Eisenberg