使用组合地图的Haskell多态递归会导致无限类型错误 [英] Haskell Polymorphic Recursion with Composed Maps causes Infinite Type Error

问题描述

这会导致一个错误（fmap也会发生）：

$ b $

  createComposedMaps list =累积列表映射
其中
 accumulate（x：xs）m =累积xs（m.map） 
 accumulate [] m = m 
  

list


我回来的错误是关于无法构造无限类型：

 发生检查：无法构造无限类型：a2〜[a2] 
预期类型：（a2  - > b1） - > ; a2  - > b1 
实际类型：（a2  - > b1） - > [a2]  - > [b1] 
相关绑定包括
 m ::（a2  - > b1） - > c（绑定在dimension_filter.hs：166：27）
 accumulate :: [t1]  - > （（a2→b1）→c）→> （a2→b1）→> 
在'（。）'的第二个参数中，即'map'
在'accumulate'的第二个参数中，也就是' （m。map）'
 
发生检查：无法构造无限类型：b1〜[b1] 
预期类型：（a2  - > b1） - > a2  - > b1 
实际类型：（a2  - > b1） - > [a2]  - > [b1] 
相关绑定包括
 m ::（a2  - > b1） - > c（绑定在dimension_filter.hs：166：27）
 accumulate :: [t1]  - > （（a2→b1）→c）→> （a2→b1）→> 
在'（。）'的第二个参数中，即'map'
在'accumulate'的第二个参数中，也就是' （m。map）'
  

目标是创建一个动态组合的映射函数，我可以稍后使用。而其他半群可以附加在一起（列表，数字......）。功能似乎更难。

希望有一个显示fmap和/或map的例子。

我发现这个库函数自己编写一个函数n次

但我需要使用每个中间构图，而不仅仅是最终构图。而一些例子仍然给我无限的类型错误。

原来这个问题可能涉及多态递归。由于 accumulate 函数的每个递归应用程序都会更改映射类型。

解决方案

这是依赖类型的典型工作，这意味着我们根据参数的值计算返回类型。在这里，我们想要表达的结果列表的嵌套取决于数字输入（在你的情况下，你使用列表参数的长度作为数字输入，但它可能更好地使用数字在需要数字） 。

不幸的是，Haskell还没有对依赖类型进行适当的支持，现有的解决方案解决方案涉及一些样板和复杂性。 是一种Haskell类语言和完全依赖类型的语言，所以我可以在Idris中说明这个想法更清晰：

   - 伊德里斯的一元自然序幕：
  -  data Nat = Z | S Nat 
 
  - 组成一个函数n次（它也可以是一个类型构造函数！）
  - 例如iterN 3 List Int = List（List（List Int））
 iterN：Nat  - > （a  - > a） - > a  - > a 
 iterN Z f a = a 
 iterN（S k）f a = f（iterN k f a）
 
 mapN：（n：Nat） - > （a  - > b） - > iterN n列出a  - > iterN n列出b 
 mapN Z f as = f as 
 mapN（S k）f as = map（mapN kf）as 
 
  -  usage：
> ; mapN 3（+10）[[[0]]] 
 [[[10]]] 
> mapN 0 id 10 
 10 
  

这是完整的Idris解决方案。在Haskell中，我们不能在类型中使用值或函数，并且使上述工作的唯一方法是创建函数的类型级版本，如类型族和值类型的单值版本，有效地写入两倍定义将是理想的。 singletons 库旨在删除批量的样板通过Haskell模板和巧妙的机器。这是一个基于单例的解决方案：

  { - ＃LANGUAGE DataKinds，TypeFamilies＃ - } 
 
 import Data.Singletons  -  package：singletons 
 import Data.Nat  -  package：singleton-nats（by me）
 
 type family IterN nfa where 
 IterN Z fa = a 
 IterN（S n）fa = f（IterN nfa）
 
 mapN :: Sing n  - > （a  - > b） - > IterN n [] a  - > IterN n [] b 
 mapN SZ f a = f a 
 mapN（SS n）f as = map（mapN n f）as 
 
  -  usage：
> mapN（sing :: SLit 3）（+10）[[[0]]] 
 [[[10]]] 
  

好消息是，正在进行的研究和开发将增加依赖类型给GHC，我们可以预计在未来几年会有所改进。

---

或者，可能会试图使用类型类来推断返回类型中的嵌套量。这非常可怕，因为我们必须区分 [a] 和非列表类型，这至少需要 OverlappingInstances ，但实际上它可以接受更糟的 IncoherentInstances ，因为我们还想根据本地上下文来解析多态类型。
$ b

  { - ＃LANGUAGE 
 UndecidableInstances，IncoherentInstances，MultiParamTypeClasses，
 FlexibleInstances，TypeFamilies＃ - } 
 
 class MapN ab as bs其中
 mapN ::（a  - > b） - > as  - > bs 
 
实例（as〜a，bs〜b）=> MapN a b as bs其中
 mapN = id 
 
实例（MapN a b as bs，bs'〜[bs]）=> MapN a b [as] bs'where 
 mapN f as = map（mapN f）as 
 
  -  usage：
> mapN（+1）0 
 1 
> mapN（+10）[[[0]]] 
 [[[10]]] 
 
  - 注意，如果没有足够的上下文`mapN`的类型是无稽之谈：
> ：t mapN（+0）
 mapN（+0）:: Num b => b  - > b 
  

What is the right way to create a function that can dynamically create composed map?

This results in an error (also happens with fmap):

createComposedMaps list = accumulate list map
    where 
        accumulate (x:xs) m = accumulate xs (m.map)
        accumulate []     m = m

The list is irrelevant, it's just there to count the number of compositions.

The error I get back is about "cannot construct infinite type":

Occurs check: cannot construct the infinite type: a2 ~ [a2]
Expected type: (a2 -> b1) -> a2 -> b1
  Actual type: (a2 -> b1) -> [a2] -> [b1]
Relevant bindings include
  m :: (a2 -> b1) -> c (bound at dimensional_filter.hs:166:27)
  accumulate :: [t1] -> ((a2 -> b1) -> c) -> (a2 -> b1) -> c
    (bound at dimensional_filter.hs:166:9)
In the second argument of ‘(.)’, namely ‘map’
In the second argument of ‘accumulate’, namely ‘(m . map)’

Occurs check: cannot construct the infinite type: b1 ~ [b1]
Expected type: (a2 -> b1) -> a2 -> b1
  Actual type: (a2 -> b1) -> [a2] -> [b1]
Relevant bindings include
  m :: (a2 -> b1) -> c (bound at dimensional_filter.hs:166:27)
  accumulate :: [t1] -> ((a2 -> b1) -> c) -> (a2 -> b1) -> c
    (bound at dimensional_filter.hs:166:9)
In the second argument of ‘(.)’, namely ‘map’
In the second argument of ‘accumulate’, namely ‘(m . map)’

The goal is to create a dynamically composed mapping function that I can later use. While other semigroups can be appended together (lists, numbers...). Functions seems to be much harder.

Would appreciate an example showing fmap and/or map.

I found this Library function to compose a function with itself n times

But I need to use each intermediate composition, not just the final composition. And some examples still gives me infinite type error.

Turns out the problem may involve polymorphic recursion. As each recursive application of the accumulate function changes the map type.

解决方案

This is a classic job for dependent types, which means that we compute return types from the values of arguments. Here we'd like to express that the nesting of the resulting list depends on a numeric input (in your case, you used the length of a list parameter as the numeric input, but it's probably better to just use numbers where numbers are needed).

Unfortunately Haskell doesn't yet have proper support for dependent typing, and existing workaround solutions involve some boilerplate and complications. Idris is a language with Haskell-like syntax and full dependent types, so I can illustrate the idea in Idris with greater clarity:

-- unary naturals from the Idris Prelude :
-- data Nat = Z | S Nat

-- compose a function n times (which can also be a type constructor!)
-- for example, iterN 3 List Int = List (List (List Int))
iterN : Nat -> (a -> a) -> a -> a
iterN Z     f a = a
iterN (S k) f a = f (iterN k f a)

mapN : (n : Nat) -> (a -> b) -> iterN n List a -> iterN n List b
mapN Z     f as = f as
mapN (S k) f as = map (mapN k f) as

-- usage:
> mapN 3 (+10) [[[0]]]
[[[10]]]
> mapN 0 id 10
10

This is the complete Idris solution. In Haskell, we can't have values or functions in types, and the only way to make the above work is to create type-level versions of functions as type families and value-level versions of types as singletons, effectively writing twice as many definitions as would be ideal. The singletons library seeks to remove the bulk of the boilerplate through Template Haskell and clever machinery. Here's a singletons-based solution:

{-# LANGUAGE DataKinds, TypeFamilies #-}

import Data.Singletons -- package: singletons
import Data.Nat        -- package: singleton-nats (by me)

type family IterN n f a where
  IterN Z     f a = a
  IterN (S n) f a = f (IterN n f a)

mapN :: Sing n -> (a -> b) -> IterN n [] a -> IterN n [] b  
mapN SZ     f a  = f a
mapN (SS n) f as = map (mapN n f) as

-- usage:
> mapN (sing :: SLit 3) (+10) [[[0]]]
[[[10]]]

The good news though is that there's ongoing research and development to add dependent types to GHC and we can expect improvements in the next few years.

---

Alternatively, one might be tempted to use type classes to infer the amount of nestedness in the return type. This is fairly horrible, because we have to distinguish [a] and non-list types, which at the very least requires OverlappingInstances, but in practice it works acceptably with the even worse IncoherentInstances, because we'd also like to resolve polymorphic types depending on the local context.

{-# LANGUAGE
  UndecidableInstances, IncoherentInstances, MultiParamTypeClasses,
  FlexibleInstances, TypeFamilies #-}

class MapN a b as bs where
  mapN :: (a -> b) -> as -> bs

instance (as ~ a, bs ~ b) => MapN a b as bs where
  mapN = id

instance (MapN a b as bs, bs' ~ [bs]) => MapN a b [as] bs' where
  mapN f as = map (mapN f) as

-- usage:
> mapN (+1) 0
1
> mapN (+10) [[[0]]]
[[[10]]]

-- note though that without enough context `mapN`'s type is nonsense:
> :t mapN (+0)
mapN (+0) :: Num b => b -> b

这篇关于使用组合地图的Haskell多态递归会导致无限类型错误的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！