<div dir="ltr">data MyContainer<br>  = MyContainer1 Item0 Item1<br>  | MyContainer2 Item0 Item1 Item2 Item3<br>  | MyContainer3 Item0 Item1 Item2 Item3 Item4 Item5 Item6<br></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Sep 5, 2023 at 4:54 PM Zoran Bošnjak <<a href="mailto:zoran.bosnjak@via.si">zoran.bosnjak@via.si</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Dear haskellers,<br>
I am trying to add some type safety to the program in the following situation:<br>
<br>
There are some distinct 'Item t' types which come in groups. That is: 'EList' container can contain either:<br>
- items 0,1<br>
- items 0,1,2,3<br>
- items 0,1,2,3,4,5,6<br>
<br>
All other combinations (like items 0,1,2) are invalid and shall be rejected by compiler. <br>
The 'EList' implementation (see below) seems to have this property.<br>
<br>
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.<br>
<br>
What is the correct implementation of mkEList?<br>
<br>
Here is a sample code and the intended usage:<br>
<br>
-- (sample build-test.hs)<br>
import GHC.TypeLits<br>
<br>
data Item (t :: Nat) = Item<br>
<br>
-- List/group of items<br>
data IList (ts :: [Nat]) where<br>
    INil  :: IList '[]<br>
    ICons :: Item t -> IList ts -> IList (t ': ts)<br>
<br>
nil :: IList '[]<br>
nil = INil<br>
<br>
infixr 5 &:<br>
(&:) :: Item t -> IList ts -> IList (t : ts)<br>
(&:) = ICons<br>
<br>
-- Extended list of groups<br>
data EList (ts :: [Nat]) (tss :: [[Nat]]) where<br>
    EList :: IList ts1 -> Maybe (EList ts2 tss) -> EList ts1 (ts2 ': tss)<br>
<br>
instance Eq (EList ts tss)<br>
<br>
-- Manual test<br>
<br>
type T1 = '[0, 1]<br>
type T2 = '[ '[2, 3], '[4, 5, 6], '[] ]<br>
<br>
test1 :: EList T1 T2<br>
test1 = EList (Item @0 &: Item @1 &: nil) Nothing<br>
<br>
test2 :: EList T1 T2<br>
test2 = EList (Item @0 &: Item @1 &: nil)<br>
    (Just (EList (Item @2 &: Item @3 &: nil) Nothing))<br>
<br>
test3 :: EList T1 T2<br>
test3 = EList (Item @0 &: Item @1 &: nil)<br>
    (Just (EList (Item @2 &: Item @3 &: nil)<br>
        (Just (EList (Item @4 &: Item @5 &: Item @6 &: nil) Nothing))))<br>
<br>
-- Intended usage<br>
<br>
-- | Helper function or class method :: IList ? -> EList ? ?<br>
mkEList :: a<br>
mkEList = undefined<br>
<br>
el1 :: EList T1 T2<br>
el1 = mkEList<br>
    ( Item @0 <br>
   &: Item @1 <br>
   &: nil) <br>
<br>
el2 :: EList T1 T2<br>
el2 = mkEList<br>
    ( Item @0 <br>
   &: Item @1 <br>
   &: Item @2 <br>
   &: Item @3<br>
   &: nil)<br>
<br>
el3 :: EList T1 T2<br>
el3 = mkEList<br>
    ( Item @0 <br>
   &: Item @1 <br>
   &: Item @2 <br>
   &: Item @3<br>
   &: Item @4 <br>
   &: Item @5 <br>
   &: Item @6<br>
   &: nil)<br>
<br>
check :: Bool -- expecting True<br>
check = and [el1 == test1, el2 == test2, el3 == test3]<br>
-- (end of sample)<br>
<br>
regards,<br>
Zoran<br>
_______________________________________________<br>
Haskell-Cafe mailing list<br>
To (un)subscribe, modify options or view archives go to:<br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe</a><br>
Only members subscribed via the mailman list are allowed to post.</blockquote></div>