Fruit salad

Salad.hs

{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

module Salad where

import           Data.Kind                    (Type)
import GHC.TypeLits

data Apple = Apple { size :: Int }
data Pear = Pear
data Banana = Banana
data Kiwi = Kiwi
data Strawberry = Strawberry
data Blueberry = Blueberry

data Fruit a where
  AnApple :: Apple -> Fruit Apple
  APear :: Pear -> Fruit Pear
  ABanana :: Banana -> Fruit Banana
  AKiwi :: Kiwi -> Fruit Kiwi
  AStrawberry :: Strawberry -> Fruit Strawberry
  ABlueberry :: Blueberry -> Fruit Blueberry

data FruitList (ts :: [Type]) where
  HNil :: FruitList '[]
  HCons :: Fruit t -> FruitList ts -> FruitList (t ': ts)

data SomeFruit = forall a. SomeFruit { getFruit :: Fruit a }

newtype Salad = Salad [SomeFruit]

class HasApples ts where
  type family NumApples ts :: Nat
  getApples :: FruitList ts -> [Fruit Apple] -- could also be a fixed-length list of length 'NumApples ts'

class HasPears ts where
  type family NumPears ts :: Nat
  getPears :: FruitList ts -> [Fruit Pear]

instance HasApples '[] where
  type NumApples '[] = 0
  getApples _ = []

instance HasApples xs => HasApples (Apple ': xs) where
  type NumApples (Apple ': xs) = 1 + NumApples xs
  getApples = \case
    HCons a xs -> a : getApples xs

instance HasApples xs => HasApples (Pear ': xs) where
  type NumApples (Pear ': xs) = NumApples xs
  getApples = \case
    HCons _ xs -> getApples xs

instance HasApples xs => HasApples (Banana ': xs) where
  type NumApples (Banana ': xs) = NumApples xs
  getApples = \case
    HCons _ xs -> getApples xs

instance HasApples xs => HasApples (Kiwi ': xs) where
  type NumApples (Kiwi ': xs) = NumApples xs
  getApples = \case
    HCons _ xs -> getApples xs

instance HasApples xs => HasApples (Strawberry ': xs) where
  type NumApples (Strawberry ': xs) = NumApples xs
  getApples = \case
    HCons _ xs -> getApples xs

instance HasApples xs => HasApples (Blueberry ': xs) where
  type NumApples (Blueberry ': xs) = NumApples xs
  getApples = \case
    HCons _ xs -> getApples xs

instance HasPears '[] where
  type NumPears '[] = 0
  getPears _ = []

instance HasPears xs => HasPears (Pear ': xs) where
  type NumPears (Pear ': xs) = 1 + NumPears xs
  getPears = \case
    HCons a xs -> a : getPears xs

instance HasPears xs => HasPears (Apple ': xs) where
  type NumPears (Apple ': xs) = NumPears xs
  getPears = \case
    HCons _ xs -> getPears xs

instance HasPears xs => HasPears (Banana ': xs) where
  type NumPears (Banana ': xs) = NumPears xs
  getPears = \case
    HCons _ xs -> getPears xs

instance HasPears xs => HasPears (Kiwi ': xs) where
  type NumPears (Kiwi ': xs) = NumPears xs
  getPears = \case
    HCons _ xs -> getPears xs

instance HasPears xs => HasPears (Strawberry ': xs) where
  type NumPears (Strawberry ': xs) = NumPears xs
  getPears = \case
    HCons _ xs -> getPears xs

instance HasPears xs => HasPears (Blueberry ': xs) where
  type NumPears (Blueberry ': xs) = NumPears xs
  getPears = \case
    HCons _ xs -> getPears xs

fruitMixA ::
  forall xs.
  (HasApples xs
  , (NumApples xs + NumPears xs) ~ 1) -- either 1 apple or 1 pear
  => FruitList xs
  -> Salad
fruitMixA = Salad . fmap SomeFruit . getApples

-- This compiles
mixRight :: Salad
mixRight = fruitMixA $ HCons (AnApple (Apple 10)) HNil

-- This doesn't compile
mixWrong :: Salad
mixWrong = fruitMixA $ HCons (ABlueberry Blueberry) HNil

Salad2.hs

{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}

module Salad2 where

import           Data.Kind                    (Type)
import GHC.TypeLits

data Apple = Apple { size :: Int }
data Pear = Pear
data Banana = Banana
data Kiwi = Kiwi
data Strawberry = Strawberry
data Blueberry = Blueberry

data Fruit =
  AnApple Apple
  | APear Pear
  | ABanana Banana
  | AKiwi Kiwi
  | AStrawberry Strawberry
  | ABlueberry Blueberry

data LList (n :: Nat) a where
  LNil :: LList 0 a
  LCons :: a -> LList n a -> LList (n + 1) a

toList :: forall n a. LList n a -> [a]
toList = \case
  LNil -> []
  LCons x xs -> x : toList xs

data FruitBowl numApples numPears numBananas numKiwis numStrawberries numBlueberries =
  FruitBowl
    { apples :: LList numApples Apple
    , pears  :: LList numPears Pear
    , bananas :: LList numBananas Banana
    , kiwis :: LList numKiwis Kiwi
    , strawberries :: LList numStrawberries Strawberry
    , blueberries :: LList numBlueberries Blueberry
    }
  
emptyBowl :: FruitBowl 0 0 0 0 0 0
emptyBowl = FruitBowl LNil LNil LNil LNil LNil LNil

addApple ::
  forall numApples numPears numBananas numKiwis numStrawberries numBlueberries.
  Apple
  -> FruitBowl numApples numPears numBananas numKiwis numStrawberries numBlueberries
  -> FruitBowl (numApples + 1) numPears numBananas numKiwis numStrawberries numBlueberries
addApple a b@FruitBowl{apples} =
  b{apples = LCons a apples}

addPear :: 
  forall numApples numPears numBananas numKiwis numStrawberries numBlueberries.
  Pear
  -> FruitBowl numApples numPears numBananas numKiwis numStrawberries numBlueberries
  -> FruitBowl numApples (numPears + 1) numBananas numKiwis numStrawberries numBlueberries
addPear a b@FruitBowl{pears} =
  b{pears = LCons a pears}

mixA ::
  forall numApples numPears numBananas numKiwis numStrawberries numBlueberries.
  ( numApples <= 1, numPears <= 1, numBananas <= 1, numKiwis <= 1, numStrawberries <= 1, numBlueberries <= 1
  , (numApples + numPears) ~ 1
  )
  => FruitBowl numApples numPears numBananas numKiwis numStrawberries numBlueberries
  -> [Fruit]
mixA FruitBowl{apples} =
  AnApple <$> toList apples

mixRight :: [Fruit]
mixRight = mixA $ addApple (Apple 10) emptyBowl

mixWrong :: [Fruit]
mixWrong = mixA $ addApple (Apple 10) $ addApple (Apple 20) emptyBowl