MK
Ох уж эти ваш кубики
Size: a a a
2020 November 20
MK
Придумали какую-то хрень и сидят
DB
Ох уж эти ваш кубики
это которые из 8-ми лямблд?)
AA
Знаешь, как можно Int в тип слифтить?
case someNatVal . fromIntegral $ какойтоинт of
SomeNat pn ->
MK
case someNatVal . fromIntegral $ какойтоинт of
SomeNat pn ->
Это же вроде не будет работать
AA
почему это?
MK
С символами у меня не получалось
MK
Мб что-то делал не так
MK
Но вообще как это работать может, если инт только в рантайме есть?
DB
будет работать, тип мы статически не узнаем конечно, но все нужные констрейнты получим, и написать невалидный код не выйдет
А можно тогда чуть более полный код, а то непонятно, что после кейса делать
MK
Или вы там литерал пишете?
AV
data SQ = SQ Bool SomeNat
mkQ :: Maybe SQ
mkQ 0 = Nothing
mkQ n
| n < 0 = Just $ SQ False (someNatVal (abs (n-1)))
| otherwise = Just $ SQ True (someNatVal (n-1))
fromQ :: SQ -> Integer
fromQ (SQ b s) = bool negate id b $ (1+ natVal s)
mkQ :: Maybe SQ
mkQ 0 = Nothing
mkQ n
| n < 0 = Just $ SQ False (someNatVal (abs (n-1)))
| otherwise = Just $ SQ True (someNatVal (n-1))
fromQ :: SQ -> Integer
fromQ (SQ b s) = bool negate id b $ (1+ natVal s)
AV
чота такое
к
Но вообще как это работать может, если инт только в рантайме есть?
а как завтипы работают по твоему?
AV
для хаскеля хватит