2

Idris をいじり始めたばかりで、いくつかの Haskell マシンにシューホーニングしてみました。

namespace works
  data Auto a b = AutoC (a -> (b, Auto a b))

  const_auto : b -> Auto a b
  const_auto b = AutoC (\_ => (b, const_auto b))

ただし、追加のパラメーターを使用して、モナドとして出力を生成できるように一般化Auto a bしたいと思います。私の直感では、 type が含まれるはずでしたが、タイプチェッカーはそれが一致しないと不平を言います。だから私はそれをもう少しポリモーフィックなままにしてみました：AutoM m a bmmType -> Type(Type, Type) -> Type

namespace doesntwork

  data AutoM : {x : Type } -> (m : x -> Type) -> (a : Type) -> (b : Type) -> Type where
     AutoMC : (a -> m (b, AutoM m a b)) -> AutoM m a b

  data Identity a = IdentityC a

  Auto : Type -> Type -> Type
  Auto = AutoM Identity

これは少なくとも型チェックを行います。しかし、私がしようとすると：

  const_auto : Monad m => {m : x -> Type } -> {a : Type} -> b -> AutoM m a b
  const_auto b = AutoMC (\_ => return (b, const_auto b))

しかし、それは良くありません:

When elaborating right hand side of Stream.doesntwork.const_auto:
When elaborating an application of function Prelude.Monad.return:
        Can't unify
                (A, B) (Type of (a, b))
        with
                (b, AutoM m4 a b) (Expected type)

そして、型エラーの意味がよくわかりません。の定義で がどこにも使用されていないのに、一体なぜ の型(a, b)が言及されるのでしょうか? 定義自体がすでに間違っている気がしますが、その理由や方法はよくわかりません。aconst_autoAutoM

4

1 に答える 1

4

あなたの直観mが、モナドであると type を持つべきだと言ったとき、あなたは正しかったType -> Type。ここでの問題は、型コンストラクターとデータ コンストラクターの両方を意味するように(,)オーバーロードされており、Idris のエラボレーターが間違った選択をしていることです。PairmkPair

を明示的に選択Pairすることで、定義を修正します。

data AutoM : (m : Type -> Type) -> (a : Type) -> (b : Type) -> Type where
   AutoMC : (a -> m (Pair b (AutoM m a b))) -> AutoM m a b

さて、それを行うと、別の不可解なメッセージが表示されます。

Auto.idr:18:14:
When elaborating right hand side of Main.doesntwork.const_auto:
Can't resolve type class Monad m3
Metavariables: Main.doesntwork.const_auto

ここでの問題は、制約によって既に導入されているものとは異なるm型注釈に暗黙的を導入するため、Idris はこの new のインスタンスを見つけることができないという事実です。解決策は、次のようにそれをまったく導入しないことです（スコープ内にあるのに十分であることに言及している制約）。const_autoMonad m =>Monadmm

const_auto : Monad m => {a : Type} -> b -> AutoM m a b
于 2015-07-12T21:22:13.090 に答える