runtimeValueToType.hs

-- original code is written by https://github.com/klapaucius

{-# OPTIONS -Wall -Werror #-}

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}

module Main (main) where

import Data.Singletons
import Numeric.Natural

-- | Nat -- это и тип, и кайнд (тип типов)
data Nat = Z | S Nat

-- Всё, что ниже, генерируется автоматически
-- genSingletons [''Nat]
-- но приведено для образовательных целей

-- | синглтон для Nat
data instance Sing (n :: Nat) where
    SZ :: Sing 'Z
    SS :: Sing n -> Sing ('S n)

-- | механизм трансляции между значениями типа Nat и значениями синглтон-типа
instance SingKind Nat where
    type DemoteRep Nat = Natural

    fromSing SZ = 0
    fromSing (SS n) = fromSing n + 1

    toSing 0 = SomeSing SZ
    toSing n =
        case toSing (n - 1) :: SomeSing Nat of
            SomeSing k -> SomeSing (SS k)

-- конец автоматически генерируемого бойлерплейта

-- функция создает вложенные списки (если n > 0)
mkNestedList :: Sing (n :: Nat) -> MyType n
mkNestedList SZ = 'a'
mkNestedList (SS x) = [mkNestedList x]

-- разных типов в зависимости
-- от передаваемого ей значения.
type family MyType (a :: Nat)
type instance MyType 'Z = Char
type instance MyType ('S x) = [MyType x]

-- функция сериализует в строку эти списки (разных типов)
-- тут от передаваемого значения зависит тип другого принимаемого значения
showNestedList :: Sing (n :: Nat) -> MyType n -> String
showNestedList SZ v = show v
showNestedList (SS x) v = "[" ++ concatMap (showNestedList x) v ++ "]"

main :: IO ()
main = do
    ns <- getLine -- пользователь вводит число с клавиатуры
    let n = read ns -- парсим его
    -- создаем из этого числа синглетон, дальше внутри лямбды
    -- это число будет типом.
    putStrLn $
        withSomeSing n $ \n'sing ->
            showNestedList n'sing (mkNestedList n'sing)