что простой индукцией от Z до n оно не заработает, так как конструктор Mul возвращает не (Structure (S n)), а просто (Structure n). Если возможно это сделать, то куда копать?
import Data.Type.Nat
data Structure n where
Nil :: Structure Z
Mul :: Int -> Structure n -> Structure n
Cons :: Int -> Structure n -> Structure (S n)
data SomeStructure where
MkSomeStructure :: Structure n -> SomeStructure
data Exp = ENil | EMul Int Exp | ECons Int Exp
construct :: Exp -> SomeStructure
construct exp = undefined
Попробуй ещё в конструкт синглтон передать
Обсуждают сегодня