IdrisとHaskellの差異「依存型のパターンマッチが可能」
Idrisに入門中なので、せっかくだからHaskellではできなかったけどIdrisではできること、 またその逆を定期的に挙げていきたいと思います 🐕
以下のとこには載ってないものを挙げてくつもりです!
初回なので、少し前提知識の補填が入るのはご容赦を。 ここでの主題はあくまで「依存型のパターンマッチが可能」というところです。
Index
Idrisでは依存型のパターンマッチができる
コードを見てもらえれば、感覚がわかると思う。
Vect
型については後述。
length' : Vect n a -> Nat
length' {n = val} _ = val
{n = val}
というのが依存型n
のパターンマッチである。
n
には例えばVect 5 Int
のように自然数値が入る。
その後の_
はVect n a
値が束縛されるが、既に必要ないのでアンダースコアによって破棄される。
このval
はパターンなので、例えば以下のようなマッチングもかけることができる。
(Z : Type
とS : Nat -> Type
はNat
型の値。Z
は0
、S Z
は1
を表す)
length' : Vect n a -> Nat
length' {n = Z} _ = 0
length' {n = S _} xs = 1 + length' (tail xs)
コード全文
import Data.Vect
xs : Vect 5 Int
xs = [1,2,3,4,5]
length' : Vect n a -> Nat
length' {n = val} _ = val
--length' : Vect n a -> Nat
--length' {n = Z} _ = 0
--length' {n = S _} xs = 1 + length' (tail xs)
main : IO ()
main = printLn $ length' xs
-- {output}
-- 5
Haskellで書くなら
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}
import Data.Proxy (Proxy(..))
import GHC.TypeLits
data Vect (n :: Nat) a :: * where
Nil :: Vect 0 a
(:::) :: a -> Vect n a -> Vect (n + 1) a
infixr 7 :::
xs :: Vect 5 Int
xs = 1 ::: 2 ::: 3 ::: 4 ::: 5 ::: Nil
-- HaskellではNatが値を持たないのでIntを使う
length' :: forall n a. KnownNat n => Vect n a -> Int
length' _ = fromInteger $ natVal (Proxy :: Proxy n)
main :: IO ()
main = print $ length' xs
-- {output}
-- 5
余談: 使用した諸機能の説明
以上で使用した諸機能について補足をします。
printLn
/print
Haskellでのprint
はprintLn
に該当する。
Idrisのprint
は改行を出力しない。
Vect n a
Vect
型はその長さを型パラメータn
に持つa
のリストである。
例えば以下は長さ5を持つ。
xs : Vect 5 Int
xs = [1,2,3,4,5]
Vect
の簡略的定義はこんな感じ
data Vect : Nat -> a -> Type where
Nil : Vect 0 a
(::) : x -> Vect n a -> Vect (S n) a
infixl 7 ::
またType
型はHaskellで言う*
種である。
Idrisでは値と型の区別がなく、つまり種(型の型)も値で表現できるので、
「ある自然数と要素の型を受け取り、その型を返す」
という表現はNat -> a -> Type
になる。
Idrisでの自然数(Nat
)は0
も含む
やはりプログラミングでは0
を含んだ方が、自然数がぐーーーんと使いやすい。
リストリテラル中の..
記法はVect
では使えないみたい
xs : Vect 5 Int
xs = [1..5]
| xs = [1..5]
| ~~~~~~
When checking right hand side of xs with expected type
Vect 5 Int
Type mismatch between
List a (Type of enumFromTo _ _)
and
Vect 5 Int (Expected type)
(expected type Vect 5 Int
but got List a
と言っている)
IdrisではGHCのGADTs
拡張相当がデフォルトで使える
上記、Vect
の簡略定義の通り。
もちろん普通の代数的データ型もこんな感じに書ける。
data Mine = My String