Idrisに入門中なので、せっかくだからHaskellではできなかったけどIdrisではできること、 またその逆を定期的に挙げていきたいと思います 🐕
以下のとこには載ってないものを挙げてくつもりです!
初回なので、少し前提知識の補填が入るのはご容赦を。 ここでの主題はあくまで「依存型のパターンマッチが可能」というところです。
Index
Idrisでは依存型のパターンマッチができる
コードを見てもらえれば、感覚がわかると思う。 Vect
型については後述。
{n = val}
というのが依存型n
のパターンマッチである。 n
には例えばVect 5 Int
のように自然数値が入る。
その後の_
はVect n a
値が束縛されるが、既に必要ないのでアンダースコアによって破棄される。
このval
はパターンなので、例えば以下のようなマッチングもかけることができる。
(Z : Type
とS : Nat -> Type
はNat
型の値。Z
は0
、S Z
は1
を表す)
コード全文
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を持つ。
Vect
の簡略的定義はこんな感じ
またType
型はHaskellで言う*
種である。
Idrisでは値と型の区別がなく、つまり種(型の型)も値で表現できるので、 「ある自然数と要素の型を受け取り、その型を返す」 という表現はNat -> a -> Type
になる。
Idrisでの自然数(Nat
)は0
も含む
やはりプログラミングでは0
を含んだ方が、自然数がぐーーーんと使いやすい。
リストリテラル中の..
記法はVect
では使えないみたい
| 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
の簡略定義の通り。
もちろん普通の代数的データ型もこんな感じに書ける。
この記事はこちらから修正リクエストを送ることができます。
IdrisとHaskellの差異「依存型のパターンマッチが可能」 - github
ゴミ箱ボタンの左にある、鉛筆ボタンを押してね!