在GHCi中输入家族神经节 [英] Type Family Shenanigans in GHCi

问题描述

以下是我的代码：

  { - ＃LANGUAGE TypeFamilies，TypeOperators，DataKinds，PolyKinds，FlexibleContexts，UndecidableInstances＃ - } 
 
模块Foo其中
 
导入Data.Singletons.Prelude 
导入Data.Type.Equality 
 
数据TP ab 
 $ （bool&（r == x），r））（True，head xs）xs 
 type family same（b :: bool）（r :: k）（rq :: [k]）:: k其中
相同的bool r（x'：xs）=相同（bool：&&（r == x） ）r xs 
相同的bool r'[] = TP bool r 
 
数据NotEqualFailure 
  - 将True结果转换为类型
类型系列EqResult tp其中
 EqResult（TP'True r）= r 
 EqResult（TP'False r）= NotEqualFailure 
 
 
 
 data Zq qi 
 type family Foo rq 
类型实例Foo（Zq qi）= i 
类型R = 
 EqResult 
（相同'True（Foo（Zq Double Int））
（Map TyCon1 Foo）
'[Zq Double Int，Zq Float Int]））
 
f :: R 
f = 3 
  

GHC 7.8.3 ：

 没有使用'f'引起的（Num NotEqualFailure）
 
在表达式：f 
在'it'的等式中：it = f 
  

但是如果我注释掉 f 并开始GHCi：

 > ：类！ R 
 R :: * 
 = Int 
  

以确定我的列表中的元素是否相等。如果它们相等， EqResult 应该返回通用类型（这里是 Int ），否则返回 NotEqualFailure 。任何人都可以解释这里发生了什么？如果你也认为这看起来像一个bug，我会把它提交到GHC trac。

如果你能想出一种方法来编写EqResult （相同...），这可能会解决这个问题。

---

编辑
我重写了这个类型的家族，但不幸的是我遇到了基本相同的问题。

  { - ＃LANGUAGE TypeFamilies，TypeOperators，DataKinds，FlexibleContexts，UndecidableInstances＃ - } 
 
 module Foo其中
 
导入Data.Singletons.Prelude 
导入Data.Singletons.Prelude.List 
导入Data.Type.Equality 
 $ （bool&（r == x），r））（True，head xs）xs 
 type family same rq where 
相同（x'：xs）= 
 EqResult（And（Map（（TyCon2（==））$ x）xs））x 
 
 data NotEqualFailure 
 - 将True结果转换为类型
类型系列EqResult bv其中
 EqResult'True r = r 
 EqResult'False r = NotEqualFailure 
 
 type R =相同'[Int，Int] 
 
f :: R 
f = 3 
  

< GHCi仍然可以解析 R 至 Int ，但GHC无法解析<$ c $的类型族c> EqResult 现在（在将它错误地解析为 NotEqualFailure 之前）。请注意，如果我将列表的大小更改为1，即'[Int] 。

---

编辑2
我删除了所有外部库，并让所有的东西都起作用。这个解决方案可能是最小的，但我仍然想知道为什么更大的例子似乎打破了GHC。

  { - ＃LANGUAGE TypeFamilies，DataKinds，
 UndecidableInstances＃ - } 
 
模块Foo其中
 
类型系列相同（rq :: [*]）:: *其中
相同（x'：xs）= EqTo x xs 
 
  - 如果x == y，则对所有x'进行测试x'xs 
类型系列EqTo y xs其中
 EqTo y （x'：xs）= NotEqualFailure 
 
数据NotEqualFailure 
 
 type R = Same'[Int，Int] 
f :: R 
f = 3 
  

nofollow>将在下一版GHC中得到修复。

Here's my code:

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, PolyKinds, FlexibleContexts, UndecidableInstances #-}

module Foo where

import Data.Singletons.Prelude
import Data.Type.Equality

data TP a b

-- foldl (\(bool, r) x -> (bool && (r == x), r)) (True, head xs) xs
type family Same (b :: Bool) (r :: k) (rq :: [k]) :: k where
  Same bool r (x ': xs) = Same (bool :&& (r == x)) r xs
  Same bool r '[] = TP bool r

data NotEqualFailure
-- converts a True result to a type
type family EqResult tp where
  EqResult (TP 'True r) = r
  EqResult (TP 'False r) = NotEqualFailure



data Zq q i
type family Foo rq
type instance Foo (Zq q i) = i
type R = 
  EqResult 
    (Same 'True (Foo (Zq Double Int)) 
      (Map (TyCon1 Foo) 
        '[Zq Double Int, Zq Float Int]))

f :: R
f = 3

This doesn't compile in GHC 7.8.3:

No instance for (Num NotEqualFailure)
      arising from a use of ‘f’
    In the expression: f
    In an equation for ‘it’: it = f

but if I comment out f and start GHCi:

> :kind! R
R :: *
= Int

So GHC can't seem to decide if the elements in my list are equal or not. If they are equal, EqResult should return the common type (Int here), otherwise it returns NotEqualFailure. Can anyone explain what's going on here? Let me know if you also think this looks like a bug, and I'll file it on the GHC trac.

If you can figure out a way to write "EqResult (Same ...)" in a different way, it might get around this issue.

---

EDIT I rewrote the type family, but unfortunately I'm having essentially the same problem. The code is smaller and simpler now.

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, FlexibleContexts, UndecidableInstances #-}

module Foo where

import Data.Singletons.Prelude
import Data.Singletons.Prelude.List
import Data.Type.Equality

-- foldl (\(bool, r) x -> (bool && (r == x), r)) (True, head xs) xs
type family Same rq where
  Same (x ': xs) = 
    EqResult (And (Map ((TyCon2 (==)) $ x) xs)) x

data NotEqualFailure
-- converts a True result to a type
type family EqResult b v where
  EqResult 'True r = r
  EqResult 'False r = NotEqualFailure

type R = Same '[Int, Int]

f :: R
f = 3

GHCi can still resolve R to Int, but GHC can't resolve the type family for EqResult at all now (before it incorrectly resolved it to NotEqualFailure). Note that this example works if I change the size of the list to one, i.e. '[Int].

---

EDIT 2 I removed all external libraries, and got everything to work. This solution is probably the smallest, but I still want to know why the larger examples appear to break GHC.

{-# LANGUAGE TypeFamilies, DataKinds,
             UndecidableInstances #-}

module Foo where

type family Same (rq :: [*]) :: * where
  Same (x ': xs) = EqTo x xs

--tests if x==y for all x\in xs
type family EqTo y xs where
  EqTo y '[] = y
  EqTo y (y ': xs) = EqTo y xs
  EqTo y (x ': xs) = NotEqualFailure

data NotEqualFailure

type R = Same '[Int, Int]
f :: R
f = 3

解决方案

There is in fact a bug, and it will be fixed in the next release of GHC.

这篇关于在GHCi中输入家族神经节的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！