入力タイプと出力タイプを同じにするにはどうすればよいですか？

Question

私は、ManningのIdrisでタイプ駆動開発を行っています。型のファミリで関数を特定の型に制限する方法を教える例を示します。我々はPedalまたはPetrolのいずれかであるPowerSourceを使用するVehicleタイプを持っており、ガソリンをその電源として使用する車両についてのみタイプチェックを行うrefillという関数を書く必要があります。

以下のコードは動作しますが、Carを補充することはCarなくBusを生成することを保証するものではありません。 Carを指定した場合にCarを生成し、Busを指定した場合はBusを生成するには、refill関数のシグネチャを変更する必要がありますか？

data PowerSource 
    = Pedal 
    | Petrol 

data Vehicle : PowerSource -> Type 
    where 
    Bicycle : Vehicle Pedal 
    Car : (fuel : Nat) -> Vehicle Petrol 
    Bus : (fuel : Nat) -> Vehicle Petrol 

refuel : Vehicle Petrol -> Nat -> Vehicle Petrol 
refuel (Car fuel) x  = Car (fuel + x) 
refuel (Bus fuel) x  = Bus (fuel + x) 

Answer 1

これは、新しいVehicleTypeデータ型を導入することにより、このようVehicleに1つの以上のパラメータを追加することによって達成することができます。

data VehicleType = BicycleT | CarT | BusT 

data Vehicle : PowerSource -> VehicleType -> Type 
    where 
    Bicycle :     Vehicle Pedal BicycleT 
    Car  : (fuel : Nat) -> Vehicle Petrol CarT 
    Bus  : (fuel : Nat) -> Vehicle Petrol BusT 

あなたは何とかコンストラクタ間の型の違いにエンコードする必要があります。型の安全性をさらに高めるには、型に情報を追加する必要があります。そして、あなたはrefuel機能を実装するためにそれを使用することができます：

refuel : Vehicle Petrol t -> Nat -> Vehicle Petrol t 
refuel (Car fuel) x  = Car (fuel + x) 
refuel (Bus fuel) x  = Bus (fuel + x) 

refuel (Car fuel) x  = Bus (fuel + x) 

で

refuel (Car fuel) x  = Car (fuel + x) 

を交換すると、次のタイプのエラーにつながる：

Type checking ./Fuel.idr 
Fuel.idr:14:8:When checking right hand side of refuel with expected type 
     Vehicle Petrol CarT 

Type mismatch between 
     Vehicle Petrol BusT (Type of Bus fuel) 
and 
     Vehicle Petrol CarT (Expected type) 

Specifically: 
     Type mismatch between 
       BusT 
     and 
       CarT 

Answer 2

別の可能性は、にあります何をするってあなたは外部にしたい。元のタイプを変更できない場合は、オプションになる可能性があります。もしそれが図書館から来たのであれば。また、多くのプロパティを追加するために追加したい余分なインデックスを持つタイプを混乱させたくない場合は、

​​3210

それでは、コンストラクタは車両を構築するために使用されたを教えてくれる関数を定義してみましょう：

は、私たちは@Shershによって導入VehicleTypeタイプを再利用してみましょう。

total 
vehicleType : Vehicle t -> VehicleType 
vehicleType Bicycle = BicycleT 
vehicleType (Car _) = CarT 
vehicleType (Bus _) = BusT 

そして今、我々はrefuelは、車両の種類を維持すると言うことができます：この回答のため

total 
refuelPreservesVehicleType : vehicleType (refuel v x) = vehicleType v 
refuelPreservesVehicleType {v = (Car _)} = Refl 
refuelPreservesVehicleType {v = (Bus _)} = Refl