Kannan Goundan writes:

Karl Voelker writes:

...

{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} module FS where

type Date = String

data FileKind = FILE | FOLDER

data Entry (k :: FileKind) where File :: String -> Date -> Int -> Entry FILE Folder :: String -> String -> Entry FOLDER

This is a little beyond my Haskell knowledge. What would the function signatures look like? Here are my guesses:

listFolder :: Path -> [Entry ?]

Unfortunately, we cannot have our cake and eat it as well. Entry FILE and Entry FOLDER are now different types, and hence you cannot construct a list containing both. In other words; we cannot really fill in the ? in the type signature (or at least not that I'm aware of). Either we use Either (pun intended): listFolder :: Path -> [Either (Entry FILE) (Entry FOLDER)] or you have to create some existential type around an Entry again, i.e. data SomeEntry where SomeEntry :: Entry k -> SomeEntry listFolder :: Path -> [SomeEntry] You can get the file kind back by pattern matching again.

createFolder :: Path -> Entry FOLDER createFile :: Path -> Entry FOLDER

the second one should produce something of type Entry FILE.

Also, lets say I wanted to just get the "id" fields from a list of `Entry` values. Can someone help me fill in the blanks here?

l :: [Entry ?] let ids = map (?) l

This is basically the same issue as before. You cannot construct a list that contains both Entry FILE and Entry FOLDER values. We can use type classes together with the SomeEntry solution above though. ---- In general I like the fact that we can use the GADTs to obtain extra type level guarantees. However, working with lists (or other data structures) with them is a crime. I think for that, we need better support for working with hetrogenious collections. -- - Frank

A potentially more elegant approach is using existential types. {-# LANGUAGE ExistentialQuantification #-} class IsFsEntry a where bar :: a -> String data FsFile = FsFile instance IsFsEntry FsFile where bar _ = "File" data FsFolder = FsFolder instance IsFsEntry FsFolder where bar _ = "Folder" data FsEntry = forall a . (IsFsEntry a) => MkFsEntry a https://gist.github.com/jcmartin/cfa5e28ba36574a7e68d James On Wed, Nov 12, 2014 at 11:13 AM, Jeffrey Brown wrote:

I am imagining an alternative idiom for heterogeneous treatment in which there is a single constructor, but the data type includes an attribute that is a dictionary keyed with function names, leading to values that are the corresponding code.

It seems like that would have to be memory-wasteful, duplicating the code in every object, since Haskell does not permit pointers to a single code source, but maybe I'm wrong about that.

On Wed, Nov 12, 2014 at 12:56 AM, Frank Staals wrote:

...

Kannan Goundan writes:

...

Karl Voelker writes:

...

{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} module FS where

type Date = String

data FileKind = FILE | FOLDER

data Entry (k :: FileKind) where File :: String -> Date -> Int -> Entry FILE Folder :: String -> String -> Entry FOLDER

This is a little beyond my Haskell knowledge. What would the function signatures look like? Here are my guesses:

listFolder :: Path -> [Entry ?]

Unfortunately, we cannot have our cake and eat it as well. Entry FILE and Entry FOLDER are now different types, and hence you cannot construct a list containing both. In other words; we cannot really fill in the ? in the type signature (or at least not that I'm aware of). Either we use Either (pun intended): listFolder :: Path -> [Either (Entry FILE) (Entry FOLDER)] or you have to create some existential type around an Entry again, i.e.

data SomeEntry where SomeEntry :: Entry k -> SomeEntry

listFolder :: Path -> [SomeEntry]

You can get the file kind back by pattern matching again.

...

createFolder :: Path -> Entry FOLDER createFile :: Path -> Entry FOLDER

the second one should produce something of type Entry FILE.

...

Also, lets say I wanted to just get the "id" fields from a list of `Entry` values. Can someone help me fill in the blanks here?

l :: [Entry ?] let ids = map (?) l

This is basically the same issue as before. You cannot construct a list that contains both Entry FILE and Entry FOLDER values. We can use type classes together with the SomeEntry solution above though.

----

In general I like the fact that we can use the GADTs to obtain extra type level guarantees. However, working with lists (or other data structures) with them is a crime. I think for that, we need better support for working with hetrogenious collections.

--

- Frank _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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

The tradeoff for using existentials: - You need to have an explicit covariance rule. It is necessary to call MkFsEntry (or in Frank's case: SomeEntry). - It is impossible to prove the contravariant case. If you give me a FsEntry, how do I convert it back to a FsFile or a FsFolder? For Frank's case, I can't create either of these functions and guarantee anything statically. convertBack :: SomeEntry -> FsEntry k or convertBack :: SomeEntry -> Either (FsEntry FILE) (FsEntry FOLDER) Or my case: convertBack :: (IsFsEntry a) => FsEntry -> a or convertBack :: FsEntry -> Either FsFile FsFolder The reason is rather simple. What if someone were to introduce a third thing that is a FsEntry, and we didn't cover that case? It is impossible to cover all possible cases because someone could come around and just add another one. We could introduce a runtime check in a similar way to how the read function works. However, we can make no static guarantee. James On Wed, Nov 12, 2014 at 6:00 PM, Jeffrey Brown wrote:

What is the tradeoff here? Would polymorphic containers prohibit the compiler from the deep reasoning it can do without them?

On Wed, Nov 12, 2014 at 12:56 AM, Frank Staals wrote:

...

Kannan Goundan writes:

...

Karl Voelker writes:

...

{-# LANGUAGE DataKinds #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} module FS where

type Date = String

data FileKind = FILE | FOLDER

data Entry (k :: FileKind) where File :: String -> Date -> Int -> Entry FILE Folder :: String -> String -> Entry FOLDER

This is a little beyond my Haskell knowledge. What would the function signatures look like? Here are my guesses:

listFolder :: Path -> [Entry ?]

Unfortunately, we cannot have our cake and eat it as well. Entry FILE and Entry FOLDER are now different types, and hence you cannot construct a list containing both. In other words; we cannot really fill in the ? in the type signature (or at least not that I'm aware of). Either we use Either (pun intended): listFolder :: Path -> [Either (Entry FILE) (Entry FOLDER)] or you have to create some existential type around an Entry again, i.e.

data SomeEntry where SomeEntry :: Entry k -> SomeEntry

listFolder :: Path -> [SomeEntry]

You can get the file kind back by pattern matching again.

...

createFolder :: Path -> Entry FOLDER createFile :: Path -> Entry FOLDER

the second one should produce something of type Entry FILE.

...

Also, lets say I wanted to just get the "id" fields from a list of `Entry` values. Can someone help me fill in the blanks here?

l :: [Entry ?] let ids = map (?) l

This is basically the same issue as before. You cannot construct a list that contains both Entry FILE and Entry FOLDER values. We can use type classes together with the SomeEntry solution above though.

----

In general I like the fact that we can use the GADTs to obtain extra type level guarantees. However, working with lists (or other data structures) with them is a crime. I think for that, we need better support for working with hetrogenious collections.

--

- Frank _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

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

On 2014-11-13 08:10, James M wrote:

I didn't explain Frank's case, only the one I constructed.

convertBack :: SomeEntry -> Either (FsEntry FILE) (FsEntry FOLDER)

For this function to work, we would need some way to inspect the type as a value, and this can only generally be done with dependent types.

convertBack :: SomeEntry -> FsEntry k

This case is technically possible to do statically, but not very useful because we have no idea what the actual type is. Therefore, we could only use it on things that work for all FsEntry and not just a subset.

We could ask for what 'k' is in the type system and perform the necessary computation in the type system. However, this is complicated, and Haskell currently only has very limited support for moving between values and types. You can look at GHC.TypeLits for an example of this.

Maybe I'm missing something, but wouldn't adding a Typeable constraint on the existential give you the option of casting back? AFAICT that should be sufficient since the FileKind is closed and you can thus just attempt both conversions and see which one succeeds. Regards,

To explain, you should think of forall (k :: FileKind) . Entry k as being different than Entry 'FOLDER Entry 'FILE The difference being that anything that is 'k' must be able to satisfy all FileKind not just one of them. James On Wed, Nov 12, 2014 at 11:47 PM, James M wrote:

This is easily testable.

deriving instance Typeable Entry deriving instance Typeable FileKind deriving instance Typeable 'FOLDER deriving instance Typeable 'FILE

convertBack :: SomeEntry -> Either (Entry FILE) (Entry FOLDER) convertBack (SomeEntry x) | typeOf x == typeOf (Folder "" "") = Right x | otherwise = Left x

The error I get is this:

Couldn't match type 'k' with ''FOLDER' 'k' is a rigid type variable bound by a pattern with constructor SomeEntry :: forall (k :: FileKind). Entry k -> SomeEntry, in an equation for 'convertBack' at cafe2.hs:24:14 Expected type: Entry 'FOLDER Actual type: Entry k Relevant bindings include x :: Entry k (bound at cafe2.hs:24:24) In the first argument of 'Right', namely 'x' In the expression: Right x

James

On Wed, Nov 12, 2014 at 11:29 PM, Bardur Arantsson wrote:

...

On 2014-11-13 08:10, James M wrote:

...

I didn't explain Frank's case, only the one I constructed.

convertBack :: SomeEntry -> Either (FsEntry FILE) (FsEntry FOLDER)

For this function to work, we would need some way to inspect the type as a value, and this can only generally be done with dependent types.

convertBack :: SomeEntry -> FsEntry k

This case is technically possible to do statically, but not very useful because we have no idea what the actual type is. Therefore, we could only use it on things that work for all FsEntry and not just a subset.

We could ask for what 'k' is in the type system and perform the necessary computation in the type system. However, this is complicated, and Haskell currently only has very limited support for moving between values and types. You can look at GHC.TypeLits for an example of this.

Maybe I'm missing something, but wouldn't adding a Typeable constraint on the existential give you the option of casting back? AFAICT that should be sufficient since the FileKind is closed and you can thus just attempt both conversions and see which one succeeds.

Regards,

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

Interesting. I wasn't aware that you could pattern match on something with different types. This would make GADTs more useful than the ExistentialTypes extension in cases where you don't need the extensibility. James On Thu, Nov 13, 2014 at 1:11 AM, Frank Staals wrote:

James M writes:

...

This is easily testable.

deriving instance Typeable Entry deriving instance Typeable FileKind deriving instance Typeable 'FOLDER deriving instance Typeable 'FILE

convertBack :: SomeEntry -> Either (Entry FILE) (Entry FOLDER) convertBack (SomeEntry x) | typeOf x == typeOf (Folder "" "") = Right x | otherwise = Left x

If the goal is just to write the `convertBack' function with the type signature above you don't need Typeable. If you enable the GADT extension you can just pattern match on the Entry that is stored in the SomeEntry, even though they have different types: i.e.

convertBack :: SomeEntry -> Either (Entry FILE) (Entry FOLDER) convertBack (SomeEntry f@(File _ _ _)) = Left f -- By pattern matching on f we -- can convince the compiler -- that f is of type Entry FILE convertBack (SomeEntry d@(Folder _ _)) = Right d

Similarly we can write a function

convertAsFile :: SomeEntry -> Entry FILE convertAsFile (SomeEntry f@(File _ _ _)) = f convertAsFile (SomeEntry d) = error "We cannot convert from a Entry FOLDER"

however there is no way of making that function total (i.e. in the second case there is no proper way of constructing an Entry FILE from an Entry FOLDER)

Because you can (locally) recover the type by pattern matching on a GADT I prefer to use GADTs to model existential types rather than using the ExistentialTypes extension.

--

- Frank