考虑:
x `f` y = x >>= (return . y)
这个功能f看起来很相似,<$>和flip liftM,但<$>似乎并没有工作,我不得不定义中缀运算符flip liftM,使它看起来不错,我假设一个已经存在？
有没有我所描述的功能,它是什么？
我一直在使用DataKinds扩展来Nat以类型安全的方式将类型级别传递给函数,我只是想知道是否有更好的编写方式:
(Proxy :: Proxy 42)
例如,是否有将自动促进字面任何扩展42到(Proxy :: Proxy 42)如果类型系统看到参数需要呢？
我以为我在某个地方看过一个,但我现在找不到它.(Proxy :: Proxy 42)我认为让用户写作有点难看.
我知道我可以提升Bool到这样的水平,Bool可能在哪里True或False:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
type family TF t :: Bool
type instance TF Int = True
type instance TF Bool = False
我想要推广(),当然只有一个价值().但这似乎不起作用:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
type family TF t :: ()
type instance TF Int = ()
type instance TF Bool = ()
我想我可以使用Bool和True,但是有一种值得提升的类型吗？
这是我正在尝试编写代码的一个简化的,也许是愚蠢的例子(这更复杂,涉及列表长度的编译时编码).
鉴于以下内容:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
data D (a :: Bool) where
D :: Bool -> D a
我想要以下功能g:
g :: D a -> Bool
g (D x) = x == a
当然,这不会编译为a类型,而不是值.
这是一个可能的解决方案:
class C (a :: Bool) where
f :: D a -> Bool
instance C True where
f (D x) = x == True
instance C False where
f (D x) = x == False …在以下代码中,我可以替换什么x = ....请注意,我不想对类进行限制a(当然,无论如何a都是类似的Bool,所以只能采用两种类型中的一种).
{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE KindSignatures #-}
data D (a :: Bool) where
D1 :: D True
D2 :: D False
x :: D a
x = ...
基本上,对于像这样的GADT,很容易在输入上做多态(只是在相应的构造函数上匹配),但我想在输出中使用多态.
在下面的代码,T1并T2编译罚款,但T3失败:
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
type family F a
data T1 b where
T1 :: a -> T1 (F a)
data T2 b where
T2 :: { x2 :: a } -> T2 a
data T3 b where
T3 :: { x3 :: a } -> T3 (F a)
我想知道为什么.T3只是T1有一个命名记录.这看起来并不那么特别,因为无论如何都可以使用构造函数语法来提取它.
这些示例可能看起来很愚蠢,但在我的代码中存在约束a,例如(Show a),因此可以在提取这些值时使用这些值.
我试图把我的头包裹在GADT周围,我怀疑一些魔法正在发生,我不明白.
考虑以下:
class C t
data T a where
T :: (C a) => { getT :: a } -> T a
f :: C a => a -> ()
f = undefined
class D t where
g :: t a -> ()
instance D T where
g (T x) = f x
这一切都很好并且编译成功.
现在考虑T的稍微不同的实例定义:
instance D T where
g x = f (getT x)
这看起来与上面完全相同,但是存在编译错误.这里发生了什么事？数据类型T没有存在变量,它只有一个简单的约束,它只是构造函数,但就是这样.
请考虑以下数据类型,该类型仅用于管理:
data D where
D1 :: Int -> D
D2 :: String -> D
DJ :: D -> D -> D
也许它上面有一个功能,说toString:
{-# INLINE toString #-}
toString x = case x of
(D1 x) -> "Int: show x"
(D2 x) -> "String: show x"
(DJ x y) -> "(" ++ toString x ++ "," ++ toString y ++ ")"
(值得注意的是,我所做的与打印无关,这只是一个说明性的例子)
所以我发现通过toString这样的定义使我的程序快15倍:
{-# INLINE toString #-}
toString x = case x of
(D1 x) -> "Int: show …可以说我有以下几点：
f :: b -> a -> b
x :: b
l :: [a]
和
foldl' f x l
在恒定空间中运行。这f是适当严格的。
现在考虑我是否有：
f2 :: b -> a -> Maybe b
f2 x y = if (pred x y) then Just $! (f x y) else Nothing
将要
foldM f2 x l
可靠地在恒定空间中运行？或者我还需要做些什么来确保我有恒定的空间但仍然有短路行为Maybe？
（注意，虽然我问了这个关于 的问题Maybe，但我实际上想用 来做这个Either，但我怀疑方法是相似的）