Parametrising過「高kinded」類型伊德里斯

Question

我剛開始與伊德里斯玩耍，並試圖裏上演一些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到AutoM m a b需要一個額外的參數，以便它可以單次生成其輸出，其中m是monad。我的直覺應該是m將有類型Type -> 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)的類型，a在const_auto的定義中的任何地方都沒有使用？我有這種感覺，AutoM本身的定義已經存在過錯，但我不知道爲什麼或如何。

Answer 1

當你的直覺告訴你m是monad時，你應該有類型Type -> Type。這裏的問題是(,) is overloaded意味着Pair類型的構造函數和mkPair數據構造函數，並且Idris的elaborator做出了錯誤的選擇。

採摘明確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 

這裏的問題是，你在const_auto的類型註釋中引入了一個隱含的m，它不同於已經引入的約束Monad m =>所以伊德里斯無法找到這個新的m的Monad實例。解決的辦法是在所有不引入它（約束提的是m足夠它是在範圍內），象這樣：

const_auto : Monad m => {a : Type} -> b -> AutoM m a b