[Haskell-cafe] heterogeneous container smart constructor question

[Patrick Chilton]

data MyContainer
  = MyContainer1 Item0 Item1
  | MyContainer2 Item0 Item1 Item2 Item3
  | MyContainer3 Item0 Item1 Item2 Item3 Item4 Item5 Item6

On Tue, Sep 5, 2023 at 4:54 PM Zoran Bošnjak <zoran.bosnjak at via.si> wrote:

> Dear haskellers,
> I am trying to add some type safety to the program in the following
> situation:
>
> There are some distinct 'Item t' types which come in groups. That is:
> 'EList' container can contain either:
> - items 0,1
> - items 0,1,2,3
> - items 0,1,2,3,4,5,6
>
> All other combinations (like items 0,1,2) are invalid and shall be
> rejected by compiler.
> The 'EList' implementation (see below) seems to have this property.
>
> In addition, I would like to define a smart constructor (mkEList), to
> simplify EList construction from some linear (no groups) IList type. In
> other words, mkEList shall slice IList to proper groups. I am aware that I
> need to use a type class / type families for this. I have tried several
> approaches, but ghc was not happy with any.
>
> What is the correct implementation of mkEList?
>
> Here is a sample code and the intended usage:
>
> -- (sample build-test.hs)
> import GHC.TypeLits
>
> data Item (t :: Nat) = Item
>
> -- List/group of items
> data IList (ts :: [Nat]) where
>     INil  :: IList '[]
>     ICons :: Item t -> IList ts -> IList (t ': ts)
>
> nil :: IList '[]
> nil = INil
>
> infixr 5 &:
> (&:) :: Item t -> IList ts -> IList (t : ts)
> (&:) = ICons
>
> -- Extended list of groups
> data EList (ts :: [Nat]) (tss :: [[Nat]]) where
>     EList :: IList ts1 -> Maybe (EList ts2 tss) -> EList ts1 (ts2 ': tss)
>
> instance Eq (EList ts tss)
>
> -- Manual test
>
> type T1 = '[0, 1]
> type T2 = '[ '[2, 3], '[4, 5, 6], '[] ]
>
> test1 :: EList T1 T2
> test1 = EList (Item @0 &: Item @1 &: nil) Nothing
>
> test2 :: EList T1 T2
> test2 = EList (Item @0 &: Item @1 &: nil)
>     (Just (EList (Item @2 &: Item @3 &: nil) Nothing))
>
> test3 :: EList T1 T2
> test3 = EList (Item @0 &: Item @1 &: nil)
>     (Just (EList (Item @2 &: Item @3 &: nil)
>         (Just (EList (Item @4 &: Item @5 &: Item @6 &: nil) Nothing))))
>
> -- Intended usage
>
> -- | Helper function or class method :: IList ? -> EList ? ?
> mkEList :: a
> mkEList = undefined
>
> el1 :: EList T1 T2
> el1 = mkEList
>     ( Item @0
>    &: Item @1
>    &: nil)
>
> el2 :: EList T1 T2
> el2 = mkEList
>     ( Item @0
>    &: Item @1
>    &: Item @2
>    &: Item @3
>    &: nil)
>
> el3 :: EList T1 T2
> el3 = mkEList
>     ( Item @0
>    &: Item @1
>    &: Item @2
>    &: Item @3
>    &: Item @4
>    &: Item @5
>    &: Item @6
>    &: nil)
>
> check :: Bool -- expecting True
> check = and [el1 == test1, el2 == test2, el3 == test3]
> -- (end of sample)
>
> regards,
> Zoran
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20230905/62f371ed/attachment.html>