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

[James M]

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 <jmartin at eecs.berkeley.edu> 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 <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/3b1d2d77/attachment.html>