Re: [Haskell-cafe] Representing record subtypes, sort of.

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. James On Wed, Nov 12, 2014 at 7:43 PM, James M wrote:

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