Всем привет! Возможно ли реализовать функцию construct? Проблема в том,

Question

Всем привет! Возможно ли реализовать функцию construct? Проблема в том,

что простой индукцией от 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

#haskell #programming #russian

0

10.07.2021

1 ответов

12 просмотров

TOV_MULTIMASSO · Accepted Answer

TOV_MULTIMASSO

Попробуй ещё в конструкт синглтон передать

0

10.07.2021

169 похожих чатов

Всем привет! Возможно ли реализовать функцию construct? Проблема в том,

1 ответов

Похожие вопросы