L
Size: a a a
2021 April 09
MP
да пожалуй, я посмотрю на что-то без тайплевелных ужасов
MP
мне уже не очень удобно писать всякое типа "blabla"
AppendSymbol "blablabla"MP
кстати да, хорошая мысль
L
Это вполне ужасно, но даже немножечко расширяемо.
type (++) a b = AppendSymbol a b
type TShow :: k -> Symbol
type family TShow x
type instance TShow @Symbol x = TShowString x
type instance TShow @Nat x = TShowNat x
type instance TShow @Bool x = TShowBool x
type family TShowString x where
TShowString x = "\"" ++ x ++ "\""
type family TShowBool x where
TShowBool 'True = "True"
TShowBool 'False = "False"
type family TShowNat x where
TShowNat 0 = "0"
TShowNat 1 = "1"
TShowNat 2 = "2"
TShowNat 3 = "3"
TShowNat 4 = "4"
TShowNat 5 = "5"
TShowNat 6 = "6"
TShowNat 7 = "7"
TShowNat 8 = "8"
TShowNat 9 = "9"
TShowNat x = TShowNat (Div x 10) ++ TShowNat (Mod x 10)MP
Круто! Дешевле в LOC будет переехать на optparser-applicative конечно :)
AA
в машинерии для кастомных ошибок компиляции емнип был готовый шоу для типов же
AA
а, нет, его тут использовать не получится
ЗП
это же не монада Дейкстры? это же просто алгоритм Дейкстры?
https://github.com/ennocramer/monad-dijkstra
монада насколько я помню должна быть такой
https://github.com/ennocramer/monad-dijkstra
монада насколько я помню должна быть такой
Dijkstra s a = Codensity ((->) s) a
ЗП
я частичку
не пропустилK
https://hackage.haskell.org/package/base-4.15.0.0/docs/Data-Typeable.html#v:cast, если переменная
Typeable. Иначе - никакк
data X = forall a. Typeable a => X a
f :: X -> String
f (X (x :: a))
| Just Refl <- eqT @a @Int =
"int: " <> show x
| Just Refl <- eqT @a @String =
"string: " <> show x
| Just Refl <- eqT @a @Bool =
"bool: " <> show x
| otherwise = "unknown"
main = do
putStrLn (f (X (1 :: Int)))
putStrLn (f (X "hello"))
putStrLn (f (X True))
putStrLn (f (X (Just (1 :: Int))))
-- int: 1
-- string: "hello"
-- bool: True
-- unknown