heterogeneous container smart constructor question
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
On Tue, 5 Sep 2023, Zoran Bošnjak 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
What about a solution in Haskell 98: (T0, T1, Maybe (T2, T3, Maybe (T4, T5, T6))) or with custom data types: data ItemsA = ItemsA T0 T1 (Maybe ItemsB) data ItemsB = ItemsB T2 T3 (Maybe ItemsC) data ItemsC = ItemsC T4 T5 T6 ?
The example I gave was simplified. A real problem contains several other complications which makes this simple solution not practical.
There will be some generated code with several dozen of such cases (schemas). I want to keep them all in one GADT, such that I can use common code to manipulate them. This is why EList was introduced for 'Extended' container.
Another problem comes from some other container types which I did not mention before. I already have mapping from
IList to other container types (not mentioned in my mail), like
grp1 :: Group '[0, 1, ...]
grp1 = mkGroup (Item @0 &: Item @1 ... &: nil)
In my case, the IList seems like universal data type to construct other items (as long as types are properly aligned). It's very convenient from application writer perspective.
So, if at all possible, I would like to map from IList to EList.
----- Original Message -----
From: "Henning Thielemann"
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
What about a solution in Haskell 98: (T0, T1, Maybe (T2, T3, Maybe (T4, T5, T6))) or with custom data types: data ItemsA = ItemsA T0 T1 (Maybe ItemsB) data ItemsB = ItemsB T2 T3 (Maybe ItemsC) data ItemsC = ItemsC T4 T5 T6 ?
On Tue, 5 Sep 2023, Zoran Bošnjak wrote:
The example I gave was simplified. A real problem contains several other complications which makes this simple solution not practical.
I have the package non-empty, that provides the types NonEmpty.T, Optional.T and Empty.T. With them you can encode any pattern of allowed list lengths. NonEmpty means "list length forbidden", Optional means "list length permitted", Empty means "maximum allowed length". In your example length 2, 5, 8 were allowed, so the bit pattern of allowed lengths is 001001001, which you can encode by type B0 = NonEmpty.T type B1 = Optional.T type SpecialList = B0 (B0 (B1 (B0 (B0 (B1 (B0 (B0 (B1 Empty.T)))))))) https://hackage.haskell.org/package/non-empty Maybe you can adapt this idea to your problem.
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.
participants (3)
-
Henning Thielemann -
Patrick Chilton -
Zoran Bošnjak