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

[James M]

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 at 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 at fstaals.net> wrote:
>
>> Kannan Goundan <kannan at 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 at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20141112/d18527d6/attachment.html>