Proposal: Data.Proxy
Hello I propose a module called Data.Proxy into the base package containing the common Proxy type used in many different libraries (e.g. HAppS, HList, ...). Attached is the source code. - Einar Karttunen
Hi
I propose a module called Data.Proxy into the base package containing the common Proxy type used in many different libraries (e.g. HAppS, HList, ...).
Attached is the source code.
Great idea! A few questions: Proxy is very simple, so why not export it as Proxy(..) - the implementation of the data type is essential to how it works. We don't hide things like Maybe's internals. It's not an abstract data type, its a concrete one (in my mind). If you do this, then proxy is redundant, we have Proxy on its own. I would rather something like proxyOf than toProxy - this fits in slightly better with asTypeOf in the Prelude. Thanks Neil
Musasabi wrote:
data Proxy a = Proxy
I do this, only I call it "Type". Anyway, ignoring that bikeshed, it can be considered the "universal type-witness". Consider a typical type-witness: data MyType a where MyBool :: MyType Bool MyInt :: MyType Int You can use type-witnesses like this to construct a type-witness for heterogenous lists: data ListType w a where Nil :: ListType w () Cons :: w a -> ListType w b -> ListType w (a,b) So now "ListType MyType" is a witness for heterogenous lists containing only Ints and Bools. But if you want a list that can contain any type, then "ListType Type" (your "ListType Proxy") will do the trick. If you prefer classes for passing witnesses around, that's easy: class Is w a where witness :: w a instance Is (ListType w) () where witness = Nil instance (Is w a,Is (ListType w) b) => Is (ListType w) (a,b) where witness = Cons witness witness instance Is MyType Bool where witness = MyBool instance Is MyType Int where witness = MyInt You can use your list type like this: addInts :: (Is (ListType MyType) list) => list -> Int addInts = addInts' witness where addInts' :: ListType MyType list -> list -> Int addInts' Nil _ = 0 addInts' (Cons (MyType Int) wl) (i:ms) = i + addInts' wl ms addInts' (Cons _ wl) (_:ms) = addInts' wl ms addInts (True,(3,(False,(4,())))) ==> 7
On Wed, 7 Feb 2007, Musasabi wrote:
Hello
I propose a module called Data.Proxy into the base package containing the common Proxy type used in many different libraries (e.g. HAppS, HList, ...).
Perhaps Type.Proxy, creating a Type hierarchy for types with trivial values intended for type-level programming? -- flippa@flippac.org "My religion says so" explains your beliefs. But it doesn't explain why I should hold them as well, let alone be restricted by them.
On Thu, Feb 08, 2007 at 02:47:52AM +0000, Philippa Cowderoy wrote:
On Wed, 7 Feb 2007, Musasabi wrote:
Hello
I propose a module called Data.Proxy into the base package containing the common Proxy type used in many different libraries (e.g. HAppS, HList, ...).
Perhaps Type.Proxy, creating a Type hierarchy for types with trivial values intended for type-level programming?
I second this proposal. Also, due to the increasing popularity of witness types, I propose a optimization/pragmatic hint (warning, only 5 mins thought, please improve): {-# NO_PATTERN_MATCHING #-} does exactly what it says, and hints to the code generator that it can use 0 bytes to represent the value by some variation of the State# magic.
Hi
Also, due to the increasing popularity of witness types, I propose a optimization/pragmatic hint (warning, only 5 mins thought, please improve):
{-# NO_PATTERN_MATCHING #-}
does exactly what it says, and hints to the code generator that it can use 0 bytes to represent the value by some variation of the State# magic.
That pragma changes the semantics of the data type from being populated by _|_ and Proxy, to being populated by nothing. Pragma's should try not to change the semantics. Wouldn't a definition such as: data Proxy a Achieve the same effect? (Of course, we are still writing the Haskell 98 libraries, so we should just use normal data for now) Thanks Neil
On 08.02 10:53, Ross Paterson wrote:
On Thu, Feb 08, 2007 at 10:49:46AM +0000, Neil Mitchell wrote:
Wouldn't a definition such as:
data Proxy a
Achieve the same effect?
In Haskell 98,
newtype Proxy a = Proxy (Proxy a) or data Proxy a = Proxy !(Proxy a)
yield one-point types.
I think these definitions make sense. One more reason not to export the constructor so the actual implementation will be hidden. I don't have a strong opinion to Type.Proxy vs Data.Proxy, but creating a new hierarchy would probably need more consensus. - Einar Karttunen
I don't have a strong opinion to Type.Proxy vs Data.Proxy, but creating a new hierarchy would probably need more consensus.
I'd lean towards Data.Proxy, as this is an instantiable type. There may only be one value for (Proxy Int) but I can create that value and pass it to a fuction, which to me makes it data. Plus your point about a new hierarchy is a good one. -- David Roundy Department of Physics Oregon State University
Wasn't something like this recently proposed, I believe we decided on calling it Void. perhaps we could put this in the same module, since it serves a similar purpose (but takes a type argument) John -- John Meacham - ⑆repetae.net⑆john⑈
participants (8)
-
Ashley Yakeley -
David Roundy -
John Meacham -
Musasabi -
Neil Mitchell -
Philippa Cowderoy -
Ross Paterson -
Stefan O'Rear