к
(все это бы решилось завтипами как обычно,
foo :: forall (n :: Nat) -> f n
foo Zero = _
foo (Succ n) = _
)
Size: a a a
2021 February 27
R
ну вот есть тайпкласс, который заменяет матчинг по натуральным числам на типе
class Foo n
instance Foo Zero
instance Foo n => Foo (Succ n)
и мне хочется, чтобы ghc знал, что для любых значений n, Foo n есть всегда
class Foo n
instance Foo Zero
instance Foo n => Foo (Succ n)
и мне хочется, чтобы ghc знал, что для любых значений n, Foo n есть всегда
не для любых, потому что можно определить натуральное число, которое ни zero, ни succ (через data family)
KV
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
data Nat = Z | S Nat
data family AlsoANat :: nat
type family IdNat (n :: Nat) :: Nat where
IdNat 'Z = 'Z
IdNat ('S n) = 'S n
IdNat AlsoANat = AlsoANatМама, роди меня обратно...
K
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
data Nat = Z | S Nat
data family AlsoANat :: nat
type family IdNat (n :: Nat) :: Nat where
IdNat 'Z = 'Z
IdNat ('S n) = 'S n
IdNat AlsoANat = AlsoANatdata family AlsoANat :: natТак, стоп.
data families же прибиты к Type, разве нет? Единственное не-прибитое семейство это Any.R
оно тайпчекается: https://ideone.com/IG5MJT
2021 February 28
[
А в хаскеле есть генераторы рандомных чисел?
И если да, то как они могут быть чистыми?
И если да, то как они могут быть чистыми?