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
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.