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 <jeffbrown.the@gmail.com> 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 <frank@fstaals.net> wrote:

Kannan Goundan <kannan@cakoose.com> writes:

> Karl Voelker <karl <at> karlv.net> 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