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}
-- 5Haskellで書くなら
{-# 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
ゴミ箱ボタンの左にある、鉛筆ボタンを押してね！