我正在尝试编写一个函数,其返回类型取决于其输入之一的值。
在 Idris 中,这很简单:
module Dependent
IntOrChar : Bool -> Type
IntOrChar True = Int
IntOrChar False = Char
fun : (x : Bool) -> IntOrChar x
fun True = 10
fun False = 'a'
有了这些定义:
λΠ> fun True
10 : Int
λΠ> fun False
'a' : Char
我的问题是:我可以在 Haskell 中以简单的方式做类似的事情吗?
我想我可以使用类似 singletons 的东西,但我不知道如何正确使用它们。
这有效:
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
module Main where
import Data.Singletons.Prelude
type family IntOrChar (x :: Bool) where
IntOrChar True = Int
IntOrChar False = Char
fun :: SBool b -> IntOrChar b
fun b = case b of
STrue -> 10
SFalse -> 'a'
...
λ fun STrue
10
λ fun SFalse
'a'
但它要求我使用 SBool
而不是普通的 Bool
。我宁愿将其用作fun True
。
有没有办法在 Haskell 中实现与 fun : (x : Bool) -> IntOrChar x
等价的方法?
最佳答案
我打算通过提出一个更复杂的依赖类型函数(如 Idris 中卡住的门示例)以及如何在 Haskell 中实现它来增强我的问题。
但我找到了答案here 。这是使用该方法的卡住门示例,供引用。
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE RankNTypes #-}
module Door where
import Data.Kind
import Data.Singletons.Prelude
import Data.Singletons.TH
import Data.Promotion.TH
$(singletons [d|
data DoorState = DoorOpen | DoorClosed
data DoorResult = Jammed | OK
|])
$(promote [d|
tryOpen :: DoorResult -> DoorState
tryOpen Jammed = DoorClosed
tryOpen OK = DoorOpen
|])
data DoorCmd (res :: k) (s :: DoorState) (f :: k ~> DoorState) where
Open :: forall check. DoorCmd check DoorClosed TryOpenSym0
Close :: DoorCmd '() DoorOpen (ConstSym1 'DoorClosed)
Knock :: DoorCmd '() state (ConstSym1 state)
Pure :: forall (res :: k) (state_fn :: k ~> DoorState). Sing res -> DoorCmd res (state_fn @@ res) state_fn
(:>>=) :: forall (a :: k1) (b :: k2) (state1 :: DoorState) (state2_fn :: k1 ~> DoorState) (state3_fn :: k2 ~> DoorState).
DoorCmd a state1 state2_fn ->
(Sing a -> DoorCmd b (state2_fn @@ a) state3_fn) ->
DoorCmd b state1 state3_fn
doorOps :: DoorCmd '() DoorClosed (ConstSym1 'DoorClosed)
doorOps = do
Knock
result <- Open
case result of
SJammed -> Knock
SOK -> Close
where
(>>=) = (:>>=)
(>>) a k = a :>>= \_ -> k
return = Pure
关于haskell - 如何在 Haskell 中编写简单的依赖类型函数?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/51126059/