Last active
July 22, 2024 10:18
-
-
Save graninas/01e511a1323b342815b941c5af49001b to your computer and use it in GitHub Desktop.
Example of a technique for Kana
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| {-# LANGUAGE DataKinds #-} | |
| {-# LANGUAGE FlexibleInstances #-} | |
| {-# LANGUAGE FlexibleContexts #-} | |
| {-# LANGUAGE TypeApplications #-} | |
| {-# LANGUAGE TypeOperators #-} | |
| {-# LANGUAGE TypeFamilies #-} | |
| {-# LANGUAGE FunctionalDependencies #-} | |
| module Main where | |
| import GHC.TypeLits | |
| import Data.Proxy | |
| -- Existential type-level interface making information hiding | |
| data IElement where | |
| ElementWrapper :: a -> IElement | |
| -- Smart constructor | |
| type family MkElement a :: IElement where | |
| MkElement a = ElementWrapper a | |
| -- Specific implementations - elements we want to hide | |
| data Element1Impl | |
| (someData :: Nat) | |
| data Element2Impl | |
| (somethineElse :: Symbol) | |
| data Element3Impl | |
| type Element1 num = MkElement (Element1Impl num) | |
| type Element2 str = MkElement (Element2Impl str) | |
| type Element3 = MkElement Element3Impl | |
| -- Collection has no idea about what IElement is | |
| data Collection | |
| (items :: [IElement]) | |
| -- Creation of a specific collection | |
| type MyCollection = | |
| '[ Element1 1 | |
| , Element2 "abc" | |
| , Element2 "cde" | |
| , Element3 | |
| ] | |
| -- Evaluation can access the hidden types | |
| class Eval' verb noun ret | |
| | verb noun -> ret where | |
| eval' :: verb -> Proxy noun -> ret | |
| data ProcessSpecificElement = ProcessSpecificElement | |
| data TraverseElements = TraverseElements | |
| instance | |
| ( KnownNat num | |
| ) => | |
| Eval' ProcessSpecificElement (Element1Impl num) (IO ()) where | |
| eval' _ _ = do | |
| print $ "Element1Impl reached" | |
| print $ natVal $ Proxy @num | |
| instance | |
| ( KnownSymbol str | |
| ) => | |
| Eval' ProcessSpecificElement (Element2Impl str) (IO ()) where | |
| eval' _ _ = do | |
| print $ "Element2Impl reached" | |
| print $ symbolVal $ Proxy @str | |
| instance | |
| Eval' ProcessSpecificElement Element3Impl (IO ()) where | |
| eval' _ _ = do | |
| print $ "Element3Impl reached" | |
| instance | |
| Eval' TraverseElements (Collection '[]) (IO ()) where | |
| eval' _ _ = pure () | |
| instance | |
| ( Eval' ProcessSpecificElement i (IO ()) | |
| , Eval' TraverseElements (Collection items) (IO ()) | |
| ) => | |
| Eval' | |
| TraverseElements | |
| (Collection ('ElementWrapper i ': items)) | |
| (IO ()) where | |
| eval' _ _ = do | |
| eval' ProcessSpecificElement $ Proxy @i | |
| eval' TraverseElements $ Proxy @(Collection items) | |
| main = eval' TraverseElements $ Proxy @(Collection MyCollection) | |
| -- Output: | |
| -- "Element1Impl reached" | |
| -- 1 | |
| -- "Element2Impl reached" | |
| -- "abc" | |
| -- "Element2Impl reached" | |
| -- "cde" | |
| -- "Element3Impl reached" |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment